0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 21 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 125.1 s)
↳10 BOUNDS(1, n^3)
@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
gt0(Cons(x, xs), Nil) → True
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs)
gcd(Nil, Nil) → Nil
gcd(Nil, Cons(x, xs)) → Nil
gcd(Cons(x, xs), Nil) → Nil
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs))
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs))
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys))
eqList(Cons(x, xs), Nil) → False
eqList(Nil, Cons(y, ys)) → False
eqList(Nil, Nil) → True
lgth(Nil) → Nil
gt0(Nil, y) → False
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y)
goal(x, y) → gcd(x, y)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs)
monus[Ite](True, Cons(x, xs), y) → xs
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x)
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y))
@(Cons(x, xs), ys) → Cons(x, @(xs, ys)) [1]
@(Nil, ys) → ys [1]
gt0(Cons(x, xs), Nil) → True [1]
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs) [1]
gcd(Nil, Nil) → Nil [1]
gcd(Nil, Cons(x, xs)) → Nil [1]
gcd(Cons(x, xs), Nil) → Nil [1]
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs)) [1]
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs)) [1]
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys)) [1]
eqList(Cons(x, xs), Nil) → False [1]
eqList(Nil, Cons(y, ys)) → False [1]
eqList(Nil, Nil) → True [1]
lgth(Nil) → Nil [1]
gt0(Nil, y) → False [1]
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y) [1]
goal(x, y) → gcd(x, y) [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs) [0]
monus[Ite](True, Cons(x, xs), y) → xs [0]
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y) [0]
gcd[Ite](True, x, y) → x [0]
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x) [0]
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y)) [0]
@(Cons(x, xs), ys) → Cons(x, @(xs, ys)) [1]
@(Nil, ys) → ys [1]
gt0(Cons(x, xs), Nil) → True [1]
gt0(Cons(x', xs'), Cons(x, xs)) → gt0(xs', xs) [1]
gcd(Nil, Nil) → Nil [1]
gcd(Nil, Cons(x, xs)) → Nil [1]
gcd(Cons(x, xs), Nil) → Nil [1]
gcd(Cons(x', xs'), Cons(x, xs)) → gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs)) [1]
lgth(Cons(x, xs)) → @(Cons(Nil, Nil), lgth(xs)) [1]
eqList(Cons(x, xs), Cons(y, ys)) → and(eqList(x, y), eqList(xs, ys)) [1]
eqList(Cons(x, xs), Nil) → False [1]
eqList(Nil, Cons(y, ys)) → False [1]
eqList(Nil, Nil) → True [1]
lgth(Nil) → Nil [1]
gt0(Nil, y) → False [1]
monus(x, y) → monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y) [1]
goal(x, y) → gcd(x, y) [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
monus[Ite](False, Cons(x', xs'), Cons(x, xs)) → monus(xs', xs) [0]
monus[Ite](True, Cons(x, xs), y) → xs [0]
gcd[Ite](False, x, y) → gcd[False][Ite](gt0(x, y), x, y) [0]
gcd[Ite](True, x, y) → x [0]
gcd[False][Ite](False, x, y) → gcd(monus(y, x), x) [0]
gcd[False][Ite](True, x, y) → gcd(y, monus(x, y)) [0]
| @ :: Cons:Nil → Cons:Nil → Cons:Nil Cons :: Cons:Nil → Cons:Nil → Cons:Nil Nil :: Cons:Nil gt0 :: Cons:Nil → Cons:Nil → True:False True :: True:False gcd :: Cons:Nil → Cons:Nil → Cons:Nil gcd[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil eqList :: Cons:Nil → Cons:Nil → True:False lgth :: Cons:Nil → Cons:Nil and :: True:False → True:False → True:False False :: True:False monus :: Cons:Nil → Cons:Nil → Cons:Nil monus[Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil goal :: Cons:Nil → Cons:Nil → Cons:Nil gcd[False][Ite] :: True:False → Cons:Nil → Cons:Nil → Cons:Nil |
and(v0, v1) → null_and [0]
monus[Ite](v0, v1, v2) → null_monus[Ite] [0]
gcd[Ite](v0, v1, v2) → null_gcd[Ite] [0]
gcd[False][Ite](v0, v1, v2) → null_gcd[False][Ite] [0]
@(v0, v1) → null_@ [0]
gt0(v0, v1) → null_gt0 [0]
gcd(v0, v1) → null_gcd [0]
lgth(v0) → null_lgth [0]
eqList(v0, v1) → null_eqList [0]
null_and, null_monus[Ite], null_gcd[Ite], null_gcd[False][Ite], null_@, null_gt0, null_gcd, null_lgth, null_eqList
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Nil => 0
True => 2
False => 1
null_and => 0
null_monus[Ite] => 0
null_gcd[Ite] => 0
null_gcd[False][Ite] => 0
null_@ => 0
null_gt0 => 0
null_gcd => 0
null_lgth => 0
null_eqList => 0
@(z, z') -{ 1 }→ ys :|: z' = ys, ys >= 0, z = 0
@(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
@(z, z') -{ 1 }→ 1 + x + @(xs, ys) :|: z = 1 + x + xs, xs >= 0, z' = ys, ys >= 0, x >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqList(z, z') -{ 1 }→ and(eqList(x, y), eqList(xs, ys)) :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
eqList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqList(z, z') -{ 1 }→ 1 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0
eqList(z, z') -{ 1 }→ 1 :|: ys >= 0, y >= 0, z = 0, z' = 1 + y + ys
eqList(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gcd(z, z') -{ 1 }→ gcd[Ite](eqList(1 + x' + xs', 1 + x + xs), 1 + x' + xs', 1 + x + xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs'
gcd(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
gcd(z, z') -{ 1 }→ 0 :|: xs >= 0, z' = 1 + x + xs, x >= 0, z = 0
gcd(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0
gcd(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gcd[False][Ite](z, z', z'') -{ 0 }→ gcd(y, monus(x, y)) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
gcd[False][Ite](z, z', z'') -{ 0 }→ gcd(monus(y, x), x) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
gcd[False][Ite](z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
gcd[Ite](z, z', z'') -{ 0 }→ x :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
gcd[Ite](z, z', z'') -{ 0 }→ gcd[False][Ite](gt0(x, y), x, y) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
gcd[Ite](z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
goal(z, z') -{ 1 }→ gcd(x, y) :|: x >= 0, y >= 0, z = x, z' = y
gt0(z, z') -{ 1 }→ gt0(xs', xs) :|: xs >= 0, z' = 1 + x + xs, x' >= 0, xs' >= 0, x >= 0, z = 1 + x' + xs'
gt0(z, z') -{ 1 }→ 2 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 0
gt0(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
gt0(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
lgth(z) -{ 1 }→ @(1 + 0 + 0, lgth(xs)) :|: z = 1 + x + xs, xs >= 0, x >= 0
lgth(z) -{ 1 }→ 0 :|: z = 0
lgth(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
monus(z, z') -{ 1 }→ monus[Ite](eqList(lgth(y), 1 + 0 + 0), x, y) :|: x >= 0, y >= 0, z = x, z' = y
monus[Ite](z, z', z'') -{ 0 }→ xs :|: z = 2, xs >= 0, z' = 1 + x + xs, z'' = y, x >= 0, y >= 0
monus[Ite](z, z', z'') -{ 0 }→ monus(xs', xs) :|: xs >= 0, z = 1, x' >= 0, xs' >= 0, x >= 0, z' = 1 + x' + xs', z'' = 1 + x + xs
monus[Ite](z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
| eq(start(V, V1, V35),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[gt0(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[lgth(V, Out)],[V >= 0]). eq(start(V, V1, V35),0,[eqList(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[monus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[goal(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[and(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V35),0,[fun2(V, V1, V35, Out)],[V >= 0,V1 >= 0,V35 >= 0]). eq(start(V, V1, V35),0,[fun1(V, V1, V35, Out)],[V >= 0,V1 >= 0,V35 >= 0]). eq(start(V, V1, V35),0,[fun3(V, V1, V35, Out)],[V >= 0,V1 >= 0,V35 >= 0]). eq(fun(V, V1, Out),1,[fun(V3, V4, Ret1)],[Out = 1 + Ret1 + V2,V = 1 + V2 + V3,V3 >= 0,V1 = V4,V4 >= 0,V2 >= 0]). eq(fun(V, V1, Out),1,[],[Out = V5,V1 = V5,V5 >= 0,V = 0]). eq(gt0(V, V1, Out),1,[],[Out = 2,V = 1 + V6 + V7,V7 >= 0,V6 >= 0,V1 = 0]). eq(gt0(V, V1, Out),1,[gt0(V8, V9, Ret)],[Out = Ret,V9 >= 0,V1 = 1 + V10 + V9,V11 >= 0,V8 >= 0,V10 >= 0,V = 1 + V11 + V8]). eq(gcd(V, V1, Out),1,[],[Out = 0,V = 0,V1 = 0]). eq(gcd(V, V1, Out),1,[],[Out = 0,V12 >= 0,V1 = 1 + V12 + V13,V13 >= 0,V = 0]). eq(gcd(V, V1, Out),1,[],[Out = 0,V = 1 + V14 + V15,V15 >= 0,V14 >= 0,V1 = 0]). eq(gcd(V, V1, Out),1,[eqList(1 + V16 + V17, 1 + V18 + V19, Ret0),fun1(Ret0, 1 + V16 + V17, 1 + V18 + V19, Ret2)],[Out = Ret2,V19 >= 0,V1 = 1 + V18 + V19,V16 >= 0,V17 >= 0,V18 >= 0,V = 1 + V16 + V17]). eq(lgth(V, Out),1,[lgth(V20, Ret11),fun(1 + 0 + 0, Ret11, Ret3)],[Out = Ret3,V = 1 + V20 + V21,V20 >= 0,V21 >= 0]). eq(eqList(V, V1, Out),1,[eqList(V22, V23, Ret01),eqList(V24, V25, Ret12),and(Ret01, Ret12, Ret4)],[Out = Ret4,V = 1 + V22 + V24,V24 >= 0,V25 >= 0,V22 >= 0,V23 >= 0,V1 = 1 + V23 + V25]). eq(eqList(V, V1, Out),1,[],[Out = 1,V = 1 + V26 + V27,V27 >= 0,V26 >= 0,V1 = 0]). eq(eqList(V, V1, Out),1,[],[Out = 1,V28 >= 0,V29 >= 0,V = 0,V1 = 1 + V28 + V29]). eq(eqList(V, V1, Out),1,[],[Out = 2,V = 0,V1 = 0]). eq(lgth(V, Out),1,[],[Out = 0,V = 0]). eq(gt0(V, V1, Out),1,[],[Out = 1,V30 >= 0,V = 0,V1 = V30]). eq(monus(V, V1, Out),1,[lgth(V31, Ret00),eqList(Ret00, 1 + 0 + 0, Ret02),fun2(Ret02, V32, V31, Ret5)],[Out = Ret5,V32 >= 0,V31 >= 0,V = V32,V1 = V31]). eq(goal(V, V1, Out),1,[gcd(V33, V34, Ret6)],[Out = Ret6,V33 >= 0,V34 >= 0,V = V33,V1 = V34]). eq(and(V, V1, Out),0,[],[Out = 1,V = 1,V1 = 1]). eq(and(V, V1, Out),0,[],[Out = 1,V = 2,V1 = 1]). eq(and(V, V1, Out),0,[],[Out = 1,V1 = 2,V = 1]). eq(and(V, V1, Out),0,[],[Out = 2,V = 2,V1 = 2]). eq(fun2(V, V1, V35, Out),0,[monus(V36, V37, Ret7)],[Out = Ret7,V37 >= 0,V = 1,V38 >= 0,V36 >= 0,V39 >= 0,V1 = 1 + V36 + V38,V35 = 1 + V37 + V39]). eq(fun2(V, V1, V35, Out),0,[],[Out = V40,V = 2,V40 >= 0,V1 = 1 + V40 + V41,V35 = V42,V41 >= 0,V42 >= 0]). eq(fun1(V, V1, V35, Out),0,[gt0(V43, V44, Ret03),fun3(Ret03, V43, V44, Ret8)],[Out = Ret8,V1 = V43,V35 = V44,V = 1,V43 >= 0,V44 >= 0]). eq(fun1(V, V1, V35, Out),0,[],[Out = V45,V = 2,V1 = V45,V35 = V46,V45 >= 0,V46 >= 0]). eq(fun3(V, V1, V35, Out),0,[monus(V47, V48, Ret04),gcd(Ret04, V48, Ret9)],[Out = Ret9,V1 = V48,V35 = V47,V = 1,V48 >= 0,V47 >= 0]). eq(fun3(V, V1, V35, Out),0,[monus(V50, V49, Ret13),gcd(V49, Ret13, Ret10)],[Out = Ret10,V = 2,V1 = V50,V35 = V49,V50 >= 0,V49 >= 0]). eq(and(V, V1, Out),0,[],[Out = 0,V51 >= 0,V52 >= 0,V = V51,V1 = V52]). eq(fun2(V, V1, V35, Out),0,[],[Out = 0,V53 >= 0,V35 = V54,V55 >= 0,V = V53,V1 = V55,V54 >= 0]). eq(fun1(V, V1, V35, Out),0,[],[Out = 0,V56 >= 0,V35 = V57,V58 >= 0,V = V56,V1 = V58,V57 >= 0]). eq(fun3(V, V1, V35, Out),0,[],[Out = 0,V59 >= 0,V35 = V60,V61 >= 0,V = V59,V1 = V61,V60 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V62 >= 0,V63 >= 0,V = V62,V1 = V63]). eq(gt0(V, V1, Out),0,[],[Out = 0,V64 >= 0,V65 >= 0,V = V64,V1 = V65]). eq(gcd(V, V1, Out),0,[],[Out = 0,V66 >= 0,V67 >= 0,V = V66,V1 = V67]). eq(lgth(V, Out),0,[],[Out = 0,V68 >= 0,V = V68]). eq(eqList(V, V1, Out),0,[],[Out = 0,V69 >= 0,V70 >= 0,V = V69,V1 = V70]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(gt0(V,V1,Out),[V,V1],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(lgth(V,Out),[V],[Out]). input_output_vars(eqList(V,V1,Out),[V,V1],[Out]). input_output_vars(monus(V,V1,Out),[V,V1],[Out]). input_output_vars(goal(V,V1,Out),[V,V1],[Out]). input_output_vars(and(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,V35,Out),[V,V1,V35],[Out]). input_output_vars(fun1(V,V1,V35,Out),[V,V1,V35],[Out]). input_output_vars(fun3(V,V1,V35,Out),[V,V1,V35],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [and/3]
1. recursive [non_tail,multiple] : [eqList/3]
2. recursive : [fun/3]
3. recursive [non_tail] : [lgth/2]
4. recursive : [fun2/4,monus/3]
5. recursive : [gt0/3]
6. recursive : [fun1/4,fun3/4,gcd/3]
7. non_recursive : [goal/3]
8. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into and/3
1. SCC is partially evaluated into eqList/3
2. SCC is partially evaluated into fun/3
3. SCC is partially evaluated into lgth/2
4. SCC is partially evaluated into monus/3
5. SCC is partially evaluated into gt0/3
6. SCC is partially evaluated into gcd/3
7. SCC is completely evaluated into other SCCs
8. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations and/3
* CE 48 is refined into CE [49]
* CE 47 is refined into CE [50]
* CE 45 is refined into CE [51]
* CE 46 is refined into CE [52]
* CE 44 is refined into CE [53]
### Cost equations --> "Loop" of and/3
* CEs [49] --> Loop 31
* CEs [50] --> Loop 32
* CEs [51] --> Loop 33
* CEs [52] --> Loop 34
* CEs [53] --> Loop 35
### Ranking functions of CR and(V,V1,Out)
#### Partial ranking functions of CR and(V,V1,Out)
### Specialization of cost equations eqList/3
* CE 43 is refined into CE [54]
* CE 40 is refined into CE [55]
* CE 41 is refined into CE [56]
* CE 42 is refined into CE [57]
* CE 39 is refined into CE [58,59,60,61,62]
### Cost equations --> "Loop" of eqList/3
* CEs [61] --> Loop 36
* CEs [60] --> Loop 37
* CEs [59] --> Loop 38
* CEs [58] --> Loop 39
* CEs [62] --> Loop 40
* CEs [54] --> Loop 41
* CEs [55] --> Loop 42
* CEs [56] --> Loop 43
* CEs [57] --> Loop 44
### Ranking functions of CR eqList(V,V1,Out)
* RF of phase [36]: [V,V1]
* RF of phase [37,38,39]: [V,V1]
* RF of phase [40]: [V,V1]
#### Partial ranking functions of CR eqList(V,V1,Out)
* Partial RF of phase [36]:
- RF of loop [36:1,36:2]:
V
V1
* Partial RF of phase [37,38,39]:
- RF of loop [37:1,37:2,38:1,38:2,39:1,39:2]:
V
V1
* Partial RF of phase [40]:
- RF of loop [40:1,40:2]:
V
V1
### Specialization of cost equations fun/3
* CE 35 is refined into CE [63]
* CE 34 is refined into CE [64]
* CE 33 is refined into CE [65]
### Cost equations --> "Loop" of fun/3
* CEs [65] --> Loop 45
* CEs [63] --> Loop 46
* CEs [64] --> Loop 47
### Ranking functions of CR fun(V,V1,Out)
* RF of phase [45]: [V]
#### Partial ranking functions of CR fun(V,V1,Out)
* Partial RF of phase [45]:
- RF of loop [45:1]:
V
### Specialization of cost equations lgth/2
* CE 37 is refined into CE [66]
* CE 38 is refined into CE [67]
* CE 36 is refined into CE [68,69,70]
### Cost equations --> "Loop" of lgth/2
* CEs [69] --> Loop 48
* CEs [70] --> Loop 49
* CEs [68] --> Loop 50
* CEs [66,67] --> Loop 51
### Ranking functions of CR lgth(V,Out)
* RF of phase [48,49,50]: [V]
#### Partial ranking functions of CR lgth(V,Out)
* Partial RF of phase [48,49,50]:
- RF of loop [48:1,49:1,50:1]:
V
### Specialization of cost equations monus/3
* CE 23 is refined into CE [71,72,73]
* CE 22 is refined into CE [74]
* CE 21 is refined into CE [75,76,77,78,79,80]
### Cost equations --> "Loop" of monus/3
* CEs [74] --> Loop 52
* CEs [75,76,77,78,79,80] --> Loop 53
* CEs [71,72,73] --> Loop 54
### Ranking functions of CR monus(V,V1,Out)
* RF of phase [54]: [V,V1]
#### Partial ranking functions of CR monus(V,V1,Out)
* Partial RF of phase [54]:
- RF of loop [54:1]:
V
V1
### Specialization of cost equations gt0/3
* CE 20 is refined into CE [81]
* CE 17 is refined into CE [82]
* CE 19 is refined into CE [83]
* CE 18 is refined into CE [84]
### Cost equations --> "Loop" of gt0/3
* CEs [84] --> Loop 55
* CEs [81] --> Loop 56
* CEs [82] --> Loop 57
* CEs [83] --> Loop 58
### Ranking functions of CR gt0(V,V1,Out)
* RF of phase [55]: [V,V1]
#### Partial ranking functions of CR gt0(V,V1,Out)
* Partial RF of phase [55]:
- RF of loop [55:1]:
V
V1
### Specialization of cost equations gcd/3
* CE 28 is refined into CE [85]
* CE 31 is refined into CE [86]
* CE 30 is refined into CE [87]
* CE 24 is refined into CE [88,89,90]
* CE 27 is refined into CE [91,92,93]
* CE 29 is refined into CE [94]
* CE 32 is refined into CE [95]
* CE 26 is refined into CE [96,97]
* CE 25 is refined into CE [98,99]
### Cost equations --> "Loop" of gcd/3
* CEs [98,99] --> Loop 59
* CEs [96,97] --> Loop 60
* CEs [85] --> Loop 61
* CEs [93] --> Loop 62
* CEs [86] --> Loop 63
* CEs [87] --> Loop 64
* CEs [88,89,90,91,92,94,95] --> Loop 65
### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [59,60]: [V+V1-2]
#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [59,60]:
- RF of loop [59:1,60:1]:
V+V1-2
### Specialization of cost equations start/3
* CE 5 is refined into CE [100,101,102,103,104,105,106]
* CE 2 is refined into CE [107,108,109,110,111]
* CE 3 is refined into CE [112]
* CE 4 is refined into CE [113,114,115,116,117,118,119,120]
* CE 6 is refined into CE [121,122,123,124,125,126]
* CE 7 is refined into CE [127,128,129,130,131]
* CE 8 is refined into CE [132,133]
* CE 9 is refined into CE [134,135,136,137]
* CE 10 is refined into CE [138,139,140,141,142]
* CE 11 is refined into CE [143,144,145,146,147]
* CE 12 is refined into CE [148,149]
* CE 13 is refined into CE [150,151,152,153,154,155]
* CE 14 is refined into CE [156,157]
* CE 15 is refined into CE [158,159,160,161,162]
* CE 16 is refined into CE [163,164,165,166,167]
### Cost equations --> "Loop" of start/3
* CEs [139,144,152,159] --> Loop 66
* CEs [100,101,102,103,104,105,106] --> Loop 67
* CEs [166] --> Loop 68
* CEs [165] --> Loop 69
* CEs [108,113] --> Loop 70
* CEs [164] --> Loop 71
* CEs [145,146,155,160,161,163] --> Loop 72
* CEs [107,109,110,111,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133] --> Loop 73
* CEs [112,134,135,136,137,138,140,141,142,143,147,148,149,150,151,153,154,156,157,158,162,167] --> Loop 74
### Ranking functions of CR start(V,V1,V35)
#### Partial ranking functions of CR start(V,V1,V35)
Computing Bounds
=====================================
#### Cost of chains of and(V,V1,Out):
* Chain [35]: 0
with precondition: [V=1,V1=1,Out=1]
* Chain [34]: 0
with precondition: [V=1,V1=2,Out=1]
* Chain [33]: 0
with precondition: [V=2,V1=1,Out=1]
* Chain [32]: 0
with precondition: [V=2,V1=2,Out=2]
* Chain [31]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of eqList(V,V1,Out):
* Chain [44]: 1
with precondition: [V=0,V1=0,Out=2]
* Chain [43]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [42]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [41]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [multiple([40],[[multiple([37,38,39],[[multiple([36],[[44]])],[44],[43],[42]])],[multiple([36],[[44]])],[44],[43],[42],[41]])]: 1*it(40)+1*it([42])+1*it([43])+1*it([44])+5*s(1)+1*s(3)+1*s(4)+1*s(5)+1*s(6)+1*s(7)+0
Such that:aux(11) =< V
aux(12) =< V+1
aux(13) =< V/2+1/2
aux(14) =< V/3+V1/3+2/3
aux(15) =< V1+1
aux(16) =< V1/2+1/2
it(40) =< aux(11)
it([42]) =< aux(11)
it([42]) =< aux(12)
it([43]) =< aux(12)
it([44]) =< aux(12)
it([42]) =< aux(13)
it([44]) =< aux(15)
s(1) =< aux(15)
it([43]) =< aux(16)
s(11) =< aux(15)* (1/2)
s(9) =< aux(14)* (6/5)
s(6) =< aux(13)
s(5) =< aux(14)
s(3) =< s(9)
s(4) =< s(9)
s(5) =< s(9)
s(4) =< aux(15)
s(5) =< aux(15)
s(7) =< aux(15)
s(7) =< s(11)
s(5) =< s(1)* (1/3)+aux(14)
s(3) =< s(1)* (1/5)+s(9)
s(4) =< s(1)* (1/5)+s(9)
s(5) =< s(1)* (1/5)+s(9)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [multiple([37,38,39],[[multiple([36],[[44]])],[44],[43],[42]])]: 1*it(37)+1*it(38)+1*it(39)+1*it([42])+1*it([43])+3*it([44])+0
Such that:aux(3) =< V/2+1/2
aux(4) =< V/3+V1/3
aux(5) =< 2/5*V+2/5*V1
aux(6) =< V1
aux(7) =< V1+1
aux(8) =< V1/2+1/2
it([42]) =< aux(3)
it(39) =< aux(4)
it(37) =< aux(5)
it(38) =< aux(5)
it(39) =< aux(5)
it(38) =< aux(6)
it(39) =< aux(6)
it([43]) =< aux(6)
it([44]) =< aux(7)
it([43]) =< aux(8)
it(39) =< it([44])* (1/3)+aux(4)
it(37) =< it([44])* (1/5)+aux(5)
it(38) =< it([44])* (1/5)+aux(5)
it(39) =< it([44])* (1/5)+aux(5)
with precondition: [Out=1,V>=1,V1>=1,V+V1>=3]
* Chain [multiple([36],[[44]])]: 1*it(36)+1*it([44])+0
Such that:it(36) =< V1
it([44]) =< V1+1
with precondition: [Out=2,V=V1,V>=1]
#### Cost of chains of fun(V,V1,Out):
* Chain [[45],47]: 1*it(45)+1
Such that:it(45) =< -V1+Out
with precondition: [V+V1=Out,V>=1,V1>=0]
* Chain [[45],46]: 1*it(45)+0
Such that:it(45) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [47]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [46]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of lgth(V,Out):
* Chain [[48,49,50],51]: 6*it(48)+1
Such that:aux(21) =< V
it(48) =< aux(21)
with precondition: [V>=1,Out>=0,V>=Out]
* Chain [51]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of monus(V,V1,Out):
* Chain [[54],53]: 3*it(54)+3*s(47)+1*s(48)+14*s(49)+1*s(52)+1*s(53)+1*s(54)+1*s(55)+2*s(56)+25*s(58)+1*s(68)+1*s(69)+1*s(70)+2*s(74)+1*s(75)+1*s(76)+1*s(77)+1*s(88)+1*s(89)+1*s(90)+12*s(126)+1*s(127)+1*s(128)+1*s(129)+1*s(130)+1*s(131)+3*s(132)+3
Such that:aux(25) =< 1
aux(26) =< 2
s(41) =< 1/2
s(64) =< V1+3
aux(41) =< V
aux(42) =< V1
aux(43) =< V1+1
aux(44) =< 2*V1+2
s(47) =< aux(25)
s(49) =< aux(26)
s(58) =< aux(42)
s(68) =< aux(42)
s(68) =< aux(43)
s(69) =< aux(43)
s(70) =< aux(43)
s(70) =< aux(26)
s(69) =< aux(25)
s(50) =< aux(26)* (1/2)
s(73) =< s(64)* (6/5)
s(74) =< aux(43)
s(75) =< s(64)
s(76) =< s(73)
s(77) =< s(73)
s(75) =< s(73)
s(77) =< aux(26)
s(75) =< aux(26)
s(56) =< aux(26)
s(56) =< s(50)
s(75) =< s(49)* (1/3)+s(64)
s(76) =< s(49)* (1/5)+s(73)
s(77) =< s(49)* (1/5)+s(73)
s(75) =< s(49)* (1/5)+s(73)
s(48) =< aux(25)
s(48) =< aux(26)
s(51) =< aux(25)* (6/5)
s(52) =< s(41)
s(53) =< aux(25)
s(54) =< s(51)
s(55) =< s(51)
s(53) =< s(51)
s(55) =< aux(26)
s(53) =< aux(26)
s(53) =< s(49)* (1/3)+aux(25)
s(54) =< s(49)* (1/5)+s(51)
s(55) =< s(49)* (1/5)+s(51)
s(53) =< s(49)* (1/5)+s(51)
s(88) =< aux(43)
s(89) =< aux(44)
s(90) =< aux(44)
s(88) =< aux(44)
s(90) =< aux(25)
s(88) =< aux(25)
s(88) =< s(49)* (1/3)+aux(43)
s(89) =< s(49)* (1/5)+aux(44)
s(90) =< s(49)* (1/5)+aux(44)
s(88) =< s(49)* (1/5)+aux(44)
aux(31) =< aux(41)
it(54) =< aux(41)
aux(31) =< aux(42)
it(54) =< aux(42)
aux(31) =< aux(44)
it(54) =< aux(44)
aux(34) =< aux(42)* (1/2)+1/2
s(133) =< it(54)*aux(42)
s(136) =< aux(31)*2
aux(35) =< it(54)*aux(34)
s(134) =< aux(35)* (4/5)
s(135) =< aux(35)* (2/3)
s(127) =< aux(35)
s(128) =< s(135)
s(129) =< s(134)
s(130) =< s(134)
s(128) =< s(134)
s(130) =< aux(31)
s(128) =< aux(31)
s(131) =< aux(31)
s(132) =< s(136)
s(128) =< s(132)* (1/3)+s(135)
s(129) =< s(132)* (1/5)+s(134)
s(130) =< s(132)* (1/5)+s(134)
s(128) =< s(132)* (1/5)+s(134)
s(126) =< s(133)
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[54],52]: 3*it(54)+12*s(126)+1*s(127)+1*s(128)+1*s(129)+1*s(130)+1*s(131)+3*s(132)+6*s(140)+1*s(141)+1*s(142)+2
Such that:s(141) =< 1
s(142) =< 2
aux(37) =< V
aux(38) =< V-Out
aux(45) =< V1
s(140) =< aux(45)
aux(31) =< aux(37)
it(54) =< aux(37)
aux(31) =< aux(38)
it(54) =< aux(38)
aux(31) =< aux(45)
it(54) =< aux(45)
aux(34) =< aux(45)* (1/2)+1/2
s(133) =< it(54)*aux(45)
s(136) =< aux(31)*2
aux(35) =< it(54)*aux(34)
s(134) =< aux(35)* (4/5)
s(135) =< aux(35)* (2/3)
s(127) =< aux(35)
s(128) =< s(135)
s(129) =< s(134)
s(130) =< s(134)
s(128) =< s(134)
s(130) =< aux(31)
s(128) =< aux(31)
s(131) =< aux(31)
s(132) =< s(136)
s(128) =< s(132)* (1/3)+s(135)
s(129) =< s(132)* (1/5)+s(134)
s(130) =< s(132)* (1/5)+s(134)
s(128) =< s(132)* (1/5)+s(134)
s(126) =< s(133)
with precondition: [V1>=2,Out>=0,V>=Out+2]
* Chain [53]: 3*s(47)+1*s(48)+14*s(49)+1*s(52)+1*s(53)+1*s(54)+1*s(55)+2*s(56)+25*s(58)+1*s(68)+1*s(69)+1*s(70)+2*s(74)+1*s(75)+1*s(76)+1*s(77)+1*s(88)+1*s(89)+1*s(90)+3
Such that:s(41) =< 1/2
s(62) =< V1+1
s(64) =< V1/3+1
s(82) =< V1/3+1/3
s(83) =< 2/5*V1+2/5
aux(25) =< 1
aux(26) =< 2
aux(27) =< V1
aux(28) =< V1/2+1/2
s(47) =< aux(25)
s(49) =< aux(26)
s(58) =< aux(27)
s(68) =< aux(27)
s(68) =< s(62)
s(69) =< s(62)
s(70) =< s(62)
s(68) =< aux(28)
s(70) =< aux(26)
s(69) =< aux(25)
s(50) =< aux(26)* (1/2)
s(73) =< s(64)* (6/5)
s(74) =< aux(28)
s(75) =< s(64)
s(76) =< s(73)
s(77) =< s(73)
s(75) =< s(73)
s(77) =< aux(26)
s(75) =< aux(26)
s(56) =< aux(26)
s(56) =< s(50)
s(75) =< s(49)* (1/3)+s(64)
s(76) =< s(49)* (1/5)+s(73)
s(77) =< s(49)* (1/5)+s(73)
s(75) =< s(49)* (1/5)+s(73)
s(48) =< aux(25)
s(48) =< aux(26)
s(51) =< aux(25)* (6/5)
s(52) =< s(41)
s(53) =< aux(25)
s(54) =< s(51)
s(55) =< s(51)
s(53) =< s(51)
s(55) =< aux(26)
s(53) =< aux(26)
s(53) =< s(49)* (1/3)+aux(25)
s(54) =< s(49)* (1/5)+s(51)
s(55) =< s(49)* (1/5)+s(51)
s(53) =< s(49)* (1/5)+s(51)
s(88) =< s(82)
s(89) =< s(83)
s(90) =< s(83)
s(88) =< s(83)
s(90) =< aux(25)
s(88) =< aux(25)
s(88) =< s(49)* (1/3)+s(82)
s(89) =< s(49)* (1/5)+s(83)
s(90) =< s(49)* (1/5)+s(83)
s(88) =< s(49)* (1/5)+s(83)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [52]: 6*s(140)+1*s(141)+1*s(142)+2
Such that:s(141) =< 1
s(142) =< 2
s(139) =< V1
s(140) =< s(139)
with precondition: [V1>=1,Out>=0,V>=Out+1]
#### Cost of chains of gt0(V,V1,Out):
* Chain [[55],58]: 1*it(55)+1
Such that:it(55) =< V1
with precondition: [Out=1,V>=1,V1>=1]
* Chain [[55],57]: 1*it(55)+1
Such that:it(55) =< V1
with precondition: [Out=2,V>=2,V1>=1]
* Chain [[55],56]: 1*it(55)+0
Such that:it(55) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [58]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [57]: 1
with precondition: [V1=0,Out=2,V>=1]
* Chain [56]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gcd(V,V1,Out):
* Chain [[59,60],65]: 30*it(59)+24*s(251)+4*s(252)+4*s(253)+4*s(254)+5*s(255)+1*s(298)+1*s(299)+1*s(300)+1*s(301)+2*s(704)+3*s(705)+3*s(706)+3*s(707)+4*s(708)+16*s(709)+128*s(710)+60*s(712)+2*s(713)+4*s(714)+4*s(715)+2*s(716)+2*s(717)+2*s(718)+8*s(719)+4*s(720)+4*s(721)+4*s(722)+4*s(723)+4*s(724)+2*s(725)+2*s(726)+2*s(727)+6*s(728)+1*s(729)+1*s(730)+1*s(731)+1*s(732)+2*s(733)+6*s(734)+12*s(735)+2*s(736)+6*s(737)+2*s(738)+2*s(739)+2*s(740)+2*s(741)+2*s(742)+2*s(743)+1*s(744)+1*s(745)+1*s(746)+6*s(750)+2*s(751)+2*s(752)+2*s(753)+2*s(754)+2*s(755)+6*s(756)+24*s(757)+1*s(822)+1*s(823)+1*s(824)+1*s(825)+12*s(828)+2
Such that:s(287) =< V+V1+2
aux(59) =< 2*V+2*V1
aux(88) =< V/3+V1/3
aux(121) =< V+V1
aux(122) =< V+V1+1
it(59) =< aux(121)
s(255) =< aux(121)
s(255) =< aux(122)
s(251) =< aux(122)
s(295) =< aux(122)* (1/2)
s(296) =< s(287)* (6/5)
s(298) =< s(287)
s(299) =< s(296)
s(300) =< s(296)
s(298) =< s(296)
s(300) =< aux(122)
s(298) =< aux(122)
s(301) =< aux(122)
s(301) =< s(295)
s(298) =< s(251)* (1/3)+s(287)
s(299) =< s(251)* (1/5)+s(296)
s(300) =< s(251)* (1/5)+s(296)
s(298) =< s(251)* (1/5)+s(296)
s(252) =< aux(121)
s(253) =< aux(59)
s(254) =< aux(59)
s(252) =< aux(59)
s(254) =< aux(121)
s(252) =< s(251)* (1/3)+aux(121)
s(253) =< s(251)* (1/5)+aux(59)
s(254) =< s(251)* (1/5)+aux(59)
s(252) =< s(251)* (1/5)+aux(59)
aux(93) =< aux(121)+1
aux(86) =< aux(121)
aux(89) =< aux(88)
aux(97) =< aux(121)+3
aux(87) =< aux(121)* (1/2)+1/2
s(791) =< aux(121)* (1/2)
s(781) =< aux(121)*2
aux(90) =< it(59)*aux(88)
aux(94) =< it(59)*aux(93)
s(762) =< it(59)*aux(86)
aux(91) =< it(59)*aux(89)
aux(100) =< it(59)*aux(97)
s(758) =< aux(90)* (6/5)
s(775) =< it(59)*aux(87)
s(760) =< aux(94)* (1/2)
s(771) =< aux(91)* (6/5)
s(776) =< aux(94)* (2/5)
s(777) =< aux(94)* (1/3)
s(780) =< aux(100)* (1/3)
s(789) =< aux(94)*2
s(710) =< s(762)
s(712) =< s(781)
s(713) =< s(762)
s(713) =< aux(94)
s(714) =< aux(94)
s(715) =< aux(94)
s(715) =< s(781)
s(714) =< aux(121)
s(794) =< s(781)* (1/2)
s(792) =< aux(100)* (6/5)
s(709) =< aux(94)
s(716) =< aux(100)
s(717) =< s(792)
s(718) =< s(792)
s(716) =< s(792)
s(718) =< s(781)
s(716) =< s(781)
s(719) =< s(781)
s(719) =< s(794)
s(716) =< s(712)* (1/3)+aux(100)
s(717) =< s(712)* (1/5)+s(792)
s(718) =< s(712)* (1/5)+s(792)
s(716) =< s(712)* (1/5)+s(792)
s(720) =< aux(121)
s(720) =< s(781)
s(790) =< aux(121)* (6/5)
s(721) =< s(791)
s(722) =< aux(121)
s(723) =< s(790)
s(724) =< s(790)
s(722) =< s(790)
s(724) =< s(781)
s(722) =< s(781)
s(722) =< s(712)* (1/3)+aux(121)
s(723) =< s(712)* (1/5)+s(790)
s(724) =< s(712)* (1/5)+s(790)
s(722) =< s(712)* (1/5)+s(790)
s(725) =< aux(94)
s(726) =< s(789)
s(727) =< s(789)
s(725) =< s(789)
s(727) =< aux(121)
s(725) =< aux(121)
s(725) =< s(712)* (1/3)+aux(94)
s(726) =< s(712)* (1/5)+s(789)
s(727) =< s(712)* (1/5)+s(789)
s(725) =< s(712)* (1/5)+s(789)
s(787) =< s(762)
s(728) =< s(762)
s(787) =< s(789)
s(728) =< s(789)
s(865) =< s(728)*aux(121)
s(786) =< s(787)*2
s(870) =< s(728)*aux(87)
s(866) =< s(870)* (4/5)
s(867) =< s(870)* (2/3)
s(822) =< s(870)
s(823) =< s(867)
s(824) =< s(866)
s(825) =< s(866)
s(823) =< s(866)
s(825) =< s(787)
s(823) =< s(787)
s(733) =< s(787)
s(734) =< s(786)
s(823) =< s(734)* (1/3)+s(867)
s(824) =< s(734)* (1/5)+s(866)
s(825) =< s(734)* (1/5)+s(866)
s(823) =< s(734)* (1/5)+s(866)
s(828) =< s(865)
s(736) =< s(762)
s(736) =< aux(94)
s(736) =< s(760)
s(779) =< s(780)* (6/5)
s(737) =< s(760)
s(738) =< s(780)
s(739) =< s(779)
s(740) =< s(779)
s(738) =< s(779)
s(740) =< s(781)
s(738) =< s(781)
s(738) =< s(712)* (1/3)+s(780)
s(739) =< s(712)* (1/5)+s(779)
s(740) =< s(712)* (1/5)+s(779)
s(738) =< s(712)* (1/5)+s(779)
s(741) =< s(777)
s(742) =< s(776)
s(743) =< s(776)
s(741) =< s(776)
s(743) =< aux(121)
s(741) =< aux(121)
s(741) =< s(712)* (1/3)+s(777)
s(742) =< s(712)* (1/5)+s(776)
s(743) =< s(712)* (1/5)+s(776)
s(741) =< s(712)* (1/5)+s(776)
s(705) =< aux(91)
s(706) =< s(771)
s(707) =< s(771)
s(705) =< s(771)
s(707) =< s(762)
s(705) =< s(762)
s(708) =< s(762)
s(708) =< s(760)
s(705) =< s(709)* (1/3)+aux(91)
s(706) =< s(709)* (1/5)+s(771)
s(707) =< s(709)* (1/5)+s(771)
s(705) =< s(709)* (1/5)+s(771)
s(767) =< s(762)
s(750) =< s(762)
s(767) =< aux(121)
s(750) =< aux(121)
s(763) =< s(750)*aux(121)
s(766) =< s(767)*2
s(768) =< s(750)*aux(87)
s(764) =< s(768)* (4/5)
s(765) =< s(768)* (2/3)
s(751) =< s(768)
s(752) =< s(765)
s(753) =< s(764)
s(754) =< s(764)
s(752) =< s(764)
s(754) =< s(767)
s(752) =< s(767)
s(755) =< s(767)
s(756) =< s(766)
s(752) =< s(756)* (1/3)+s(765)
s(753) =< s(756)* (1/5)+s(764)
s(754) =< s(756)* (1/5)+s(764)
s(752) =< s(756)* (1/5)+s(764)
s(757) =< s(763)
s(466) =< aux(86)* (1/2)+1/2
s(783) =< s(728)*aux(86)
s(788) =< s(728)*s(466)
s(784) =< s(788)* (4/5)
s(785) =< s(788)* (2/3)
s(729) =< s(788)
s(730) =< s(785)
s(731) =< s(784)
s(732) =< s(784)
s(730) =< s(784)
s(732) =< s(787)
s(730) =< s(787)
s(730) =< s(734)* (1/3)+s(785)
s(731) =< s(734)* (1/5)+s(784)
s(732) =< s(734)* (1/5)+s(784)
s(730) =< s(734)* (1/5)+s(784)
s(735) =< s(783)
s(704) =< s(775)
s(744) =< aux(90)
s(745) =< s(758)
s(746) =< s(758)
s(744) =< s(758)
s(746) =< s(762)
s(744) =< s(762)
s(744) =< s(709)* (1/3)+aux(90)
s(745) =< s(709)* (1/5)+s(758)
s(746) =< s(709)* (1/5)+s(758)
s(744) =< s(709)* (1/5)+s(758)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[59,60],64]: 26*it(59)+2*s(704)+3*s(705)+3*s(706)+3*s(707)+4*s(708)+16*s(709)+128*s(710)+60*s(712)+2*s(713)+4*s(714)+4*s(715)+2*s(716)+2*s(717)+2*s(718)+8*s(719)+4*s(720)+4*s(721)+4*s(722)+4*s(723)+4*s(724)+2*s(725)+2*s(726)+2*s(727)+6*s(728)+1*s(729)+1*s(730)+1*s(731)+1*s(732)+2*s(733)+6*s(734)+12*s(735)+2*s(736)+6*s(737)+2*s(738)+2*s(739)+2*s(740)+2*s(741)+2*s(742)+2*s(743)+1*s(744)+1*s(745)+1*s(746)+6*s(750)+2*s(751)+2*s(752)+2*s(753)+2*s(754)+2*s(755)+6*s(756)+24*s(757)+1*s(822)+1*s(823)+1*s(824)+1*s(825)+12*s(828)+1
Such that:aux(88) =< V/3+V1/3
aux(123) =< V+V1
it(59) =< aux(123)
aux(93) =< aux(123)+1
aux(86) =< aux(123)
aux(89) =< aux(88)
aux(97) =< aux(123)+3
aux(87) =< aux(123)* (1/2)+1/2
s(791) =< aux(123)* (1/2)
s(781) =< aux(123)*2
aux(90) =< it(59)*aux(88)
aux(94) =< it(59)*aux(93)
s(762) =< it(59)*aux(86)
aux(91) =< it(59)*aux(89)
aux(100) =< it(59)*aux(97)
s(758) =< aux(90)* (6/5)
s(775) =< it(59)*aux(87)
s(760) =< aux(94)* (1/2)
s(771) =< aux(91)* (6/5)
s(776) =< aux(94)* (2/5)
s(777) =< aux(94)* (1/3)
s(780) =< aux(100)* (1/3)
s(789) =< aux(94)*2
s(710) =< s(762)
s(712) =< s(781)
s(713) =< s(762)
s(713) =< aux(94)
s(714) =< aux(94)
s(715) =< aux(94)
s(715) =< s(781)
s(714) =< aux(123)
s(794) =< s(781)* (1/2)
s(792) =< aux(100)* (6/5)
s(709) =< aux(94)
s(716) =< aux(100)
s(717) =< s(792)
s(718) =< s(792)
s(716) =< s(792)
s(718) =< s(781)
s(716) =< s(781)
s(719) =< s(781)
s(719) =< s(794)
s(716) =< s(712)* (1/3)+aux(100)
s(717) =< s(712)* (1/5)+s(792)
s(718) =< s(712)* (1/5)+s(792)
s(716) =< s(712)* (1/5)+s(792)
s(720) =< aux(123)
s(720) =< s(781)
s(790) =< aux(123)* (6/5)
s(721) =< s(791)
s(722) =< aux(123)
s(723) =< s(790)
s(724) =< s(790)
s(722) =< s(790)
s(724) =< s(781)
s(722) =< s(781)
s(722) =< s(712)* (1/3)+aux(123)
s(723) =< s(712)* (1/5)+s(790)
s(724) =< s(712)* (1/5)+s(790)
s(722) =< s(712)* (1/5)+s(790)
s(725) =< aux(94)
s(726) =< s(789)
s(727) =< s(789)
s(725) =< s(789)
s(727) =< aux(123)
s(725) =< aux(123)
s(725) =< s(712)* (1/3)+aux(94)
s(726) =< s(712)* (1/5)+s(789)
s(727) =< s(712)* (1/5)+s(789)
s(725) =< s(712)* (1/5)+s(789)
s(787) =< s(762)
s(728) =< s(762)
s(787) =< s(789)
s(728) =< s(789)
s(865) =< s(728)*aux(123)
s(786) =< s(787)*2
s(870) =< s(728)*aux(87)
s(866) =< s(870)* (4/5)
s(867) =< s(870)* (2/3)
s(822) =< s(870)
s(823) =< s(867)
s(824) =< s(866)
s(825) =< s(866)
s(823) =< s(866)
s(825) =< s(787)
s(823) =< s(787)
s(733) =< s(787)
s(734) =< s(786)
s(823) =< s(734)* (1/3)+s(867)
s(824) =< s(734)* (1/5)+s(866)
s(825) =< s(734)* (1/5)+s(866)
s(823) =< s(734)* (1/5)+s(866)
s(828) =< s(865)
s(736) =< s(762)
s(736) =< aux(94)
s(736) =< s(760)
s(779) =< s(780)* (6/5)
s(737) =< s(760)
s(738) =< s(780)
s(739) =< s(779)
s(740) =< s(779)
s(738) =< s(779)
s(740) =< s(781)
s(738) =< s(781)
s(738) =< s(712)* (1/3)+s(780)
s(739) =< s(712)* (1/5)+s(779)
s(740) =< s(712)* (1/5)+s(779)
s(738) =< s(712)* (1/5)+s(779)
s(741) =< s(777)
s(742) =< s(776)
s(743) =< s(776)
s(741) =< s(776)
s(743) =< aux(123)
s(741) =< aux(123)
s(741) =< s(712)* (1/3)+s(777)
s(742) =< s(712)* (1/5)+s(776)
s(743) =< s(712)* (1/5)+s(776)
s(741) =< s(712)* (1/5)+s(776)
s(705) =< aux(91)
s(706) =< s(771)
s(707) =< s(771)
s(705) =< s(771)
s(707) =< s(762)
s(705) =< s(762)
s(708) =< s(762)
s(708) =< s(760)
s(705) =< s(709)* (1/3)+aux(91)
s(706) =< s(709)* (1/5)+s(771)
s(707) =< s(709)* (1/5)+s(771)
s(705) =< s(709)* (1/5)+s(771)
s(767) =< s(762)
s(750) =< s(762)
s(767) =< aux(123)
s(750) =< aux(123)
s(763) =< s(750)*aux(123)
s(766) =< s(767)*2
s(768) =< s(750)*aux(87)
s(764) =< s(768)* (4/5)
s(765) =< s(768)* (2/3)
s(751) =< s(768)
s(752) =< s(765)
s(753) =< s(764)
s(754) =< s(764)
s(752) =< s(764)
s(754) =< s(767)
s(752) =< s(767)
s(755) =< s(767)
s(756) =< s(766)
s(752) =< s(756)* (1/3)+s(765)
s(753) =< s(756)* (1/5)+s(764)
s(754) =< s(756)* (1/5)+s(764)
s(752) =< s(756)* (1/5)+s(764)
s(757) =< s(763)
s(466) =< aux(86)* (1/2)+1/2
s(783) =< s(728)*aux(86)
s(788) =< s(728)*s(466)
s(784) =< s(788)* (4/5)
s(785) =< s(788)* (2/3)
s(729) =< s(788)
s(730) =< s(785)
s(731) =< s(784)
s(732) =< s(784)
s(730) =< s(784)
s(732) =< s(787)
s(730) =< s(787)
s(730) =< s(734)* (1/3)+s(785)
s(731) =< s(734)* (1/5)+s(784)
s(732) =< s(734)* (1/5)+s(784)
s(730) =< s(734)* (1/5)+s(784)
s(735) =< s(783)
s(704) =< s(775)
s(744) =< aux(90)
s(745) =< s(758)
s(746) =< s(758)
s(744) =< s(758)
s(746) =< s(762)
s(744) =< s(762)
s(744) =< s(709)* (1/3)+aux(90)
s(745) =< s(709)* (1/5)+s(758)
s(746) =< s(709)* (1/5)+s(758)
s(744) =< s(709)* (1/5)+s(758)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[59,60],63]: 26*it(59)+2*s(704)+3*s(705)+3*s(706)+3*s(707)+4*s(708)+16*s(709)+128*s(710)+60*s(712)+2*s(713)+4*s(714)+4*s(715)+2*s(716)+2*s(717)+2*s(718)+8*s(719)+4*s(720)+4*s(721)+4*s(722)+4*s(723)+4*s(724)+2*s(725)+2*s(726)+2*s(727)+6*s(728)+1*s(729)+1*s(730)+1*s(731)+1*s(732)+2*s(733)+6*s(734)+12*s(735)+2*s(736)+6*s(737)+2*s(738)+2*s(739)+2*s(740)+2*s(741)+2*s(742)+2*s(743)+1*s(744)+1*s(745)+1*s(746)+6*s(750)+2*s(751)+2*s(752)+2*s(753)+2*s(754)+2*s(755)+6*s(756)+24*s(757)+1*s(822)+1*s(823)+1*s(824)+1*s(825)+12*s(828)+1
Such that:aux(88) =< V/3+V1/3
aux(124) =< V+V1
it(59) =< aux(124)
aux(93) =< aux(124)+1
aux(86) =< aux(124)
aux(89) =< aux(88)
aux(97) =< aux(124)+3
aux(87) =< aux(124)* (1/2)+1/2
s(791) =< aux(124)* (1/2)
s(781) =< aux(124)*2
aux(90) =< it(59)*aux(88)
aux(94) =< it(59)*aux(93)
s(762) =< it(59)*aux(86)
aux(91) =< it(59)*aux(89)
aux(100) =< it(59)*aux(97)
s(758) =< aux(90)* (6/5)
s(775) =< it(59)*aux(87)
s(760) =< aux(94)* (1/2)
s(771) =< aux(91)* (6/5)
s(776) =< aux(94)* (2/5)
s(777) =< aux(94)* (1/3)
s(780) =< aux(100)* (1/3)
s(789) =< aux(94)*2
s(710) =< s(762)
s(712) =< s(781)
s(713) =< s(762)
s(713) =< aux(94)
s(714) =< aux(94)
s(715) =< aux(94)
s(715) =< s(781)
s(714) =< aux(124)
s(794) =< s(781)* (1/2)
s(792) =< aux(100)* (6/5)
s(709) =< aux(94)
s(716) =< aux(100)
s(717) =< s(792)
s(718) =< s(792)
s(716) =< s(792)
s(718) =< s(781)
s(716) =< s(781)
s(719) =< s(781)
s(719) =< s(794)
s(716) =< s(712)* (1/3)+aux(100)
s(717) =< s(712)* (1/5)+s(792)
s(718) =< s(712)* (1/5)+s(792)
s(716) =< s(712)* (1/5)+s(792)
s(720) =< aux(124)
s(720) =< s(781)
s(790) =< aux(124)* (6/5)
s(721) =< s(791)
s(722) =< aux(124)
s(723) =< s(790)
s(724) =< s(790)
s(722) =< s(790)
s(724) =< s(781)
s(722) =< s(781)
s(722) =< s(712)* (1/3)+aux(124)
s(723) =< s(712)* (1/5)+s(790)
s(724) =< s(712)* (1/5)+s(790)
s(722) =< s(712)* (1/5)+s(790)
s(725) =< aux(94)
s(726) =< s(789)
s(727) =< s(789)
s(725) =< s(789)
s(727) =< aux(124)
s(725) =< aux(124)
s(725) =< s(712)* (1/3)+aux(94)
s(726) =< s(712)* (1/5)+s(789)
s(727) =< s(712)* (1/5)+s(789)
s(725) =< s(712)* (1/5)+s(789)
s(787) =< s(762)
s(728) =< s(762)
s(787) =< s(789)
s(728) =< s(789)
s(865) =< s(728)*aux(124)
s(786) =< s(787)*2
s(870) =< s(728)*aux(87)
s(866) =< s(870)* (4/5)
s(867) =< s(870)* (2/3)
s(822) =< s(870)
s(823) =< s(867)
s(824) =< s(866)
s(825) =< s(866)
s(823) =< s(866)
s(825) =< s(787)
s(823) =< s(787)
s(733) =< s(787)
s(734) =< s(786)
s(823) =< s(734)* (1/3)+s(867)
s(824) =< s(734)* (1/5)+s(866)
s(825) =< s(734)* (1/5)+s(866)
s(823) =< s(734)* (1/5)+s(866)
s(828) =< s(865)
s(736) =< s(762)
s(736) =< aux(94)
s(736) =< s(760)
s(779) =< s(780)* (6/5)
s(737) =< s(760)
s(738) =< s(780)
s(739) =< s(779)
s(740) =< s(779)
s(738) =< s(779)
s(740) =< s(781)
s(738) =< s(781)
s(738) =< s(712)* (1/3)+s(780)
s(739) =< s(712)* (1/5)+s(779)
s(740) =< s(712)* (1/5)+s(779)
s(738) =< s(712)* (1/5)+s(779)
s(741) =< s(777)
s(742) =< s(776)
s(743) =< s(776)
s(741) =< s(776)
s(743) =< aux(124)
s(741) =< aux(124)
s(741) =< s(712)* (1/3)+s(777)
s(742) =< s(712)* (1/5)+s(776)
s(743) =< s(712)* (1/5)+s(776)
s(741) =< s(712)* (1/5)+s(776)
s(705) =< aux(91)
s(706) =< s(771)
s(707) =< s(771)
s(705) =< s(771)
s(707) =< s(762)
s(705) =< s(762)
s(708) =< s(762)
s(708) =< s(760)
s(705) =< s(709)* (1/3)+aux(91)
s(706) =< s(709)* (1/5)+s(771)
s(707) =< s(709)* (1/5)+s(771)
s(705) =< s(709)* (1/5)+s(771)
s(767) =< s(762)
s(750) =< s(762)
s(767) =< aux(124)
s(750) =< aux(124)
s(763) =< s(750)*aux(124)
s(766) =< s(767)*2
s(768) =< s(750)*aux(87)
s(764) =< s(768)* (4/5)
s(765) =< s(768)* (2/3)
s(751) =< s(768)
s(752) =< s(765)
s(753) =< s(764)
s(754) =< s(764)
s(752) =< s(764)
s(754) =< s(767)
s(752) =< s(767)
s(755) =< s(767)
s(756) =< s(766)
s(752) =< s(756)* (1/3)+s(765)
s(753) =< s(756)* (1/5)+s(764)
s(754) =< s(756)* (1/5)+s(764)
s(752) =< s(756)* (1/5)+s(764)
s(757) =< s(763)
s(466) =< aux(86)* (1/2)+1/2
s(783) =< s(728)*aux(86)
s(788) =< s(728)*s(466)
s(784) =< s(788)* (4/5)
s(785) =< s(788)* (2/3)
s(729) =< s(788)
s(730) =< s(785)
s(731) =< s(784)
s(732) =< s(784)
s(730) =< s(784)
s(732) =< s(787)
s(730) =< s(787)
s(730) =< s(734)* (1/3)+s(785)
s(731) =< s(734)* (1/5)+s(784)
s(732) =< s(734)* (1/5)+s(784)
s(730) =< s(734)* (1/5)+s(784)
s(735) =< s(783)
s(704) =< s(775)
s(744) =< aux(90)
s(745) =< s(758)
s(746) =< s(758)
s(744) =< s(758)
s(746) =< s(762)
s(744) =< s(762)
s(744) =< s(709)* (1/3)+aux(90)
s(745) =< s(709)* (1/5)+s(758)
s(746) =< s(709)* (1/5)+s(758)
s(744) =< s(709)* (1/5)+s(758)
with precondition: [Out=0,V>=1,V1>=1,V1+2*V>=5]
* Chain [[59,60],62]: 10*it(59)+2*s(704)+3*s(705)+3*s(706)+3*s(707)+4*s(708)+16*s(709)+128*s(710)+16*s(711)+60*s(712)+2*s(713)+4*s(714)+4*s(715)+2*s(716)+2*s(717)+2*s(718)+8*s(719)+4*s(720)+4*s(721)+4*s(722)+4*s(723)+4*s(724)+2*s(725)+2*s(726)+2*s(727)+6*s(728)+1*s(729)+1*s(730)+1*s(731)+1*s(732)+2*s(733)+6*s(734)+12*s(735)+2*s(736)+6*s(737)+2*s(738)+2*s(739)+2*s(740)+2*s(741)+2*s(742)+2*s(743)+1*s(744)+1*s(745)+1*s(746)+6*s(750)+2*s(751)+2*s(752)+2*s(753)+2*s(754)+2*s(755)+6*s(756)+24*s(757)+1*s(822)+1*s(823)+1*s(824)+1*s(825)+12*s(828)+1*s(877)+1*s(878)+1
Such that:aux(88) =< V/3+V1/3
aux(125) =< V+V1
aux(126) =< V+V1+2
s(877) =< aux(125)
s(878) =< aux(126)
aux(83) =< aux(125)
it(59) =< aux(125)
aux(83) =< aux(126)
it(59) =< aux(126)
aux(93) =< aux(125)+1
aux(86) =< aux(125)
aux(89) =< aux(88)
aux(97) =< aux(125)+3
aux(87) =< aux(125)* (1/2)+1/2
s(791) =< aux(83)* (1/2)
s(781) =< aux(83)*2
aux(90) =< it(59)*aux(88)
aux(94) =< it(59)*aux(93)
s(762) =< it(59)*aux(86)
aux(91) =< it(59)*aux(89)
aux(100) =< it(59)*aux(97)
s(758) =< aux(90)* (6/5)
s(775) =< it(59)*aux(87)
s(760) =< aux(94)* (1/2)
s(771) =< aux(91)* (6/5)
s(776) =< aux(94)* (2/5)
s(777) =< aux(94)* (1/3)
s(780) =< aux(100)* (1/3)
s(789) =< aux(94)*2
s(710) =< s(762)
s(711) =< aux(83)
s(712) =< s(781)
s(713) =< s(762)
s(713) =< aux(94)
s(714) =< aux(94)
s(715) =< aux(94)
s(715) =< s(781)
s(714) =< aux(83)
s(794) =< s(781)* (1/2)
s(792) =< aux(100)* (6/5)
s(709) =< aux(94)
s(716) =< aux(100)
s(717) =< s(792)
s(718) =< s(792)
s(716) =< s(792)
s(718) =< s(781)
s(716) =< s(781)
s(719) =< s(781)
s(719) =< s(794)
s(716) =< s(712)* (1/3)+aux(100)
s(717) =< s(712)* (1/5)+s(792)
s(718) =< s(712)* (1/5)+s(792)
s(716) =< s(712)* (1/5)+s(792)
s(720) =< aux(83)
s(720) =< s(781)
s(790) =< aux(83)* (6/5)
s(721) =< s(791)
s(722) =< aux(83)
s(723) =< s(790)
s(724) =< s(790)
s(722) =< s(790)
s(724) =< s(781)
s(722) =< s(781)
s(722) =< s(712)* (1/3)+aux(83)
s(723) =< s(712)* (1/5)+s(790)
s(724) =< s(712)* (1/5)+s(790)
s(722) =< s(712)* (1/5)+s(790)
s(725) =< aux(94)
s(726) =< s(789)
s(727) =< s(789)
s(725) =< s(789)
s(727) =< aux(83)
s(725) =< aux(83)
s(725) =< s(712)* (1/3)+aux(94)
s(726) =< s(712)* (1/5)+s(789)
s(727) =< s(712)* (1/5)+s(789)
s(725) =< s(712)* (1/5)+s(789)
s(787) =< s(762)
s(728) =< s(762)
s(787) =< s(789)
s(728) =< s(789)
s(865) =< s(728)*aux(125)
s(786) =< s(787)*2
s(870) =< s(728)*aux(87)
s(866) =< s(870)* (4/5)
s(867) =< s(870)* (2/3)
s(822) =< s(870)
s(823) =< s(867)
s(824) =< s(866)
s(825) =< s(866)
s(823) =< s(866)
s(825) =< s(787)
s(823) =< s(787)
s(733) =< s(787)
s(734) =< s(786)
s(823) =< s(734)* (1/3)+s(867)
s(824) =< s(734)* (1/5)+s(866)
s(825) =< s(734)* (1/5)+s(866)
s(823) =< s(734)* (1/5)+s(866)
s(828) =< s(865)
s(736) =< s(762)
s(736) =< aux(94)
s(736) =< s(760)
s(779) =< s(780)* (6/5)
s(737) =< s(760)
s(738) =< s(780)
s(739) =< s(779)
s(740) =< s(779)
s(738) =< s(779)
s(740) =< s(781)
s(738) =< s(781)
s(738) =< s(712)* (1/3)+s(780)
s(739) =< s(712)* (1/5)+s(779)
s(740) =< s(712)* (1/5)+s(779)
s(738) =< s(712)* (1/5)+s(779)
s(741) =< s(777)
s(742) =< s(776)
s(743) =< s(776)
s(741) =< s(776)
s(743) =< aux(83)
s(741) =< aux(83)
s(741) =< s(712)* (1/3)+s(777)
s(742) =< s(712)* (1/5)+s(776)
s(743) =< s(712)* (1/5)+s(776)
s(741) =< s(712)* (1/5)+s(776)
s(705) =< aux(91)
s(706) =< s(771)
s(707) =< s(771)
s(705) =< s(771)
s(707) =< s(762)
s(705) =< s(762)
s(708) =< s(762)
s(708) =< s(760)
s(705) =< s(709)* (1/3)+aux(91)
s(706) =< s(709)* (1/5)+s(771)
s(707) =< s(709)* (1/5)+s(771)
s(705) =< s(709)* (1/5)+s(771)
s(767) =< s(762)
s(750) =< s(762)
s(767) =< aux(83)
s(750) =< aux(83)
s(763) =< s(750)*aux(125)
s(766) =< s(767)*2
s(768) =< s(750)*aux(87)
s(764) =< s(768)* (4/5)
s(765) =< s(768)* (2/3)
s(751) =< s(768)
s(752) =< s(765)
s(753) =< s(764)
s(754) =< s(764)
s(752) =< s(764)
s(754) =< s(767)
s(752) =< s(767)
s(755) =< s(767)
s(756) =< s(766)
s(752) =< s(756)* (1/3)+s(765)
s(753) =< s(756)* (1/5)+s(764)
s(754) =< s(756)* (1/5)+s(764)
s(752) =< s(756)* (1/5)+s(764)
s(757) =< s(763)
s(466) =< aux(86)* (1/2)+1/2
s(783) =< s(728)*aux(86)
s(788) =< s(728)*s(466)
s(784) =< s(788)* (4/5)
s(785) =< s(788)* (2/3)
s(729) =< s(788)
s(730) =< s(785)
s(731) =< s(784)
s(732) =< s(784)
s(730) =< s(784)
s(732) =< s(787)
s(730) =< s(787)
s(730) =< s(734)* (1/3)+s(785)
s(731) =< s(734)* (1/5)+s(784)
s(732) =< s(734)* (1/5)+s(784)
s(730) =< s(734)* (1/5)+s(784)
s(735) =< s(783)
s(704) =< s(775)
s(744) =< aux(90)
s(745) =< s(758)
s(746) =< s(758)
s(744) =< s(758)
s(746) =< s(762)
s(744) =< s(762)
s(744) =< s(709)* (1/3)+aux(90)
s(745) =< s(709)* (1/5)+s(758)
s(746) =< s(709)* (1/5)+s(758)
s(744) =< s(709)* (1/5)+s(758)
with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]
* Chain [[59,60],61]: 10*it(59)+2*s(704)+3*s(705)+3*s(706)+3*s(707)+4*s(708)+16*s(709)+128*s(710)+16*s(711)+60*s(712)+2*s(713)+4*s(714)+4*s(715)+2*s(716)+2*s(717)+2*s(718)+8*s(719)+4*s(720)+4*s(721)+4*s(722)+4*s(723)+4*s(724)+2*s(725)+2*s(726)+2*s(727)+6*s(728)+1*s(729)+1*s(730)+1*s(731)+1*s(732)+2*s(733)+6*s(734)+12*s(735)+2*s(736)+6*s(737)+2*s(738)+2*s(739)+2*s(740)+2*s(741)+2*s(742)+2*s(743)+1*s(744)+1*s(745)+1*s(746)+6*s(750)+2*s(751)+2*s(752)+2*s(753)+2*s(754)+2*s(755)+6*s(756)+24*s(757)+1*s(822)+1*s(823)+1*s(824)+1*s(825)+12*s(828)+1*s(879)+1*s(880)+1
Such that:aux(119) =< V+V1
aux(120) =< V+V1-2*Out
aux(88) =< V/3+V1/3
s(879) =< Out
s(880) =< Out+1
aux(83) =< aux(119)
it(59) =< aux(119)
aux(83) =< aux(120)
it(59) =< aux(120)
aux(93) =< aux(119)+1
aux(86) =< aux(119)
aux(89) =< aux(88)
aux(97) =< aux(119)+3
aux(87) =< aux(119)* (1/2)+1/2
s(791) =< aux(83)* (1/2)
s(781) =< aux(83)*2
aux(90) =< it(59)*aux(88)
aux(94) =< it(59)*aux(93)
s(762) =< it(59)*aux(86)
aux(91) =< it(59)*aux(89)
aux(100) =< it(59)*aux(97)
s(758) =< aux(90)* (6/5)
s(775) =< it(59)*aux(87)
s(760) =< aux(94)* (1/2)
s(771) =< aux(91)* (6/5)
s(776) =< aux(94)* (2/5)
s(777) =< aux(94)* (1/3)
s(780) =< aux(100)* (1/3)
s(789) =< aux(94)*2
s(710) =< s(762)
s(711) =< aux(83)
s(712) =< s(781)
s(713) =< s(762)
s(713) =< aux(94)
s(714) =< aux(94)
s(715) =< aux(94)
s(715) =< s(781)
s(714) =< aux(83)
s(794) =< s(781)* (1/2)
s(792) =< aux(100)* (6/5)
s(709) =< aux(94)
s(716) =< aux(100)
s(717) =< s(792)
s(718) =< s(792)
s(716) =< s(792)
s(718) =< s(781)
s(716) =< s(781)
s(719) =< s(781)
s(719) =< s(794)
s(716) =< s(712)* (1/3)+aux(100)
s(717) =< s(712)* (1/5)+s(792)
s(718) =< s(712)* (1/5)+s(792)
s(716) =< s(712)* (1/5)+s(792)
s(720) =< aux(83)
s(720) =< s(781)
s(790) =< aux(83)* (6/5)
s(721) =< s(791)
s(722) =< aux(83)
s(723) =< s(790)
s(724) =< s(790)
s(722) =< s(790)
s(724) =< s(781)
s(722) =< s(781)
s(722) =< s(712)* (1/3)+aux(83)
s(723) =< s(712)* (1/5)+s(790)
s(724) =< s(712)* (1/5)+s(790)
s(722) =< s(712)* (1/5)+s(790)
s(725) =< aux(94)
s(726) =< s(789)
s(727) =< s(789)
s(725) =< s(789)
s(727) =< aux(83)
s(725) =< aux(83)
s(725) =< s(712)* (1/3)+aux(94)
s(726) =< s(712)* (1/5)+s(789)
s(727) =< s(712)* (1/5)+s(789)
s(725) =< s(712)* (1/5)+s(789)
s(787) =< s(762)
s(728) =< s(762)
s(787) =< s(789)
s(728) =< s(789)
s(865) =< s(728)*aux(119)
s(786) =< s(787)*2
s(870) =< s(728)*aux(87)
s(866) =< s(870)* (4/5)
s(867) =< s(870)* (2/3)
s(822) =< s(870)
s(823) =< s(867)
s(824) =< s(866)
s(825) =< s(866)
s(823) =< s(866)
s(825) =< s(787)
s(823) =< s(787)
s(733) =< s(787)
s(734) =< s(786)
s(823) =< s(734)* (1/3)+s(867)
s(824) =< s(734)* (1/5)+s(866)
s(825) =< s(734)* (1/5)+s(866)
s(823) =< s(734)* (1/5)+s(866)
s(828) =< s(865)
s(736) =< s(762)
s(736) =< aux(94)
s(736) =< s(760)
s(779) =< s(780)* (6/5)
s(737) =< s(760)
s(738) =< s(780)
s(739) =< s(779)
s(740) =< s(779)
s(738) =< s(779)
s(740) =< s(781)
s(738) =< s(781)
s(738) =< s(712)* (1/3)+s(780)
s(739) =< s(712)* (1/5)+s(779)
s(740) =< s(712)* (1/5)+s(779)
s(738) =< s(712)* (1/5)+s(779)
s(741) =< s(777)
s(742) =< s(776)
s(743) =< s(776)
s(741) =< s(776)
s(743) =< aux(83)
s(741) =< aux(83)
s(741) =< s(712)* (1/3)+s(777)
s(742) =< s(712)* (1/5)+s(776)
s(743) =< s(712)* (1/5)+s(776)
s(741) =< s(712)* (1/5)+s(776)
s(705) =< aux(91)
s(706) =< s(771)
s(707) =< s(771)
s(705) =< s(771)
s(707) =< s(762)
s(705) =< s(762)
s(708) =< s(762)
s(708) =< s(760)
s(705) =< s(709)* (1/3)+aux(91)
s(706) =< s(709)* (1/5)+s(771)
s(707) =< s(709)* (1/5)+s(771)
s(705) =< s(709)* (1/5)+s(771)
s(767) =< s(762)
s(750) =< s(762)
s(767) =< aux(83)
s(750) =< aux(83)
s(763) =< s(750)*aux(119)
s(766) =< s(767)*2
s(768) =< s(750)*aux(87)
s(764) =< s(768)* (4/5)
s(765) =< s(768)* (2/3)
s(751) =< s(768)
s(752) =< s(765)
s(753) =< s(764)
s(754) =< s(764)
s(752) =< s(764)
s(754) =< s(767)
s(752) =< s(767)
s(755) =< s(767)
s(756) =< s(766)
s(752) =< s(756)* (1/3)+s(765)
s(753) =< s(756)* (1/5)+s(764)
s(754) =< s(756)* (1/5)+s(764)
s(752) =< s(756)* (1/5)+s(764)
s(757) =< s(763)
s(466) =< aux(86)* (1/2)+1/2
s(783) =< s(728)*aux(86)
s(788) =< s(728)*s(466)
s(784) =< s(788)* (4/5)
s(785) =< s(788)* (2/3)
s(729) =< s(788)
s(730) =< s(785)
s(731) =< s(784)
s(732) =< s(784)
s(730) =< s(784)
s(732) =< s(787)
s(730) =< s(787)
s(730) =< s(734)* (1/3)+s(785)
s(731) =< s(734)* (1/5)+s(784)
s(732) =< s(734)* (1/5)+s(784)
s(730) =< s(734)* (1/5)+s(784)
s(735) =< s(783)
s(704) =< s(775)
s(744) =< aux(90)
s(745) =< s(758)
s(746) =< s(758)
s(744) =< s(758)
s(746) =< s(762)
s(744) =< s(762)
s(744) =< s(709)* (1/3)+aux(90)
s(745) =< s(709)* (1/5)+s(758)
s(746) =< s(709)* (1/5)+s(758)
s(744) =< s(709)* (1/5)+s(758)
with precondition: [Out>=1,V>=Out,V1>=Out,V+V1>=2*Out+1]
* Chain [65]: 5*s(251)+4*s(252)+4*s(253)+4*s(254)+4*s(255)+17*s(256)+3*s(257)+1*s(290)+1*s(291)+1*s(292)+1*s(293)+1*s(298)+1*s(299)+1*s(300)+1*s(301)+2
Such that:s(284) =< V
s(285) =< V+1
s(287) =< V/3+V1/3+2/3
aux(57) =< V/2+1/2
aux(58) =< V/3+V1/3
aux(59) =< 2/5*V+2/5*V1
aux(60) =< V1
aux(61) =< V1+1
aux(62) =< V1/2+1/2
s(290) =< s(284)
s(291) =< s(284)
s(291) =< s(285)
s(292) =< s(285)
s(293) =< s(285)
s(291) =< aux(57)
s(293) =< aux(61)
s(256) =< aux(61)
s(292) =< aux(62)
s(295) =< aux(61)* (1/2)
s(296) =< s(287)* (6/5)
s(251) =< aux(57)
s(298) =< s(287)
s(299) =< s(296)
s(300) =< s(296)
s(298) =< s(296)
s(300) =< aux(61)
s(298) =< aux(61)
s(301) =< aux(61)
s(301) =< s(295)
s(298) =< s(256)* (1/3)+s(287)
s(299) =< s(256)* (1/5)+s(296)
s(300) =< s(256)* (1/5)+s(296)
s(298) =< s(256)* (1/5)+s(296)
s(257) =< aux(60)
s(252) =< aux(58)
s(253) =< aux(59)
s(254) =< aux(59)
s(252) =< aux(59)
s(254) =< aux(60)
s(252) =< aux(60)
s(255) =< aux(60)
s(255) =< aux(62)
s(252) =< s(256)* (1/3)+aux(58)
s(253) =< s(256)* (1/5)+aux(59)
s(254) =< s(256)* (1/5)+aux(59)
s(252) =< s(256)* (1/5)+aux(59)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [64]: 1
with precondition: [V=0,Out=0,V1>=1]
* Chain [63]: 1
with precondition: [V1=0,Out=0,V>=1]
* Chain [62]: 1*s(877)+1*s(878)+1
Such that:s(877) =< V1
s(878) =< V1+1
with precondition: [Out=0,V=V1,V>=1]
* Chain [61]: 1*s(879)+1*s(880)+1
Such that:s(879) =< V1
s(880) =< V1+1
with precondition: [V=V1,V=Out,V>=1]
#### Cost of chains of start(V,V1,V35):
* Chain [74]: 11*s(1322)+71*s(1324)+3*s(1341)+3*s(1342)+3*s(1343)+44*s(1344)+12*s(1347)+3*s(1348)+3*s(1349)+3*s(1350)+3*s(1351)+9*s(1353)+9*s(1354)+9*s(1355)+9*s(1356)+220*s(1357)+10*s(1358)+48*s(1359)+2*s(1362)+2*s(1363)+2*s(1364)+2*s(1365)+8*s(1366)+8*s(1367)+8*s(1368)+1024*s(1389)+480*s(1390)+16*s(1391)+32*s(1392)+32*s(1393)+128*s(1396)+16*s(1397)+16*s(1398)+16*s(1399)+64*s(1400)+32*s(1401)+32*s(1403)+32*s(1404)+32*s(1405)+32*s(1406)+16*s(1407)+16*s(1408)+16*s(1409)+48*s(1411)+8*s(1417)+8*s(1418)+8*s(1419)+8*s(1420)+16*s(1421)+48*s(1422)+96*s(1423)+16*s(1424)+48*s(1426)+16*s(1427)+16*s(1428)+16*s(1429)+16*s(1430)+16*s(1431)+16*s(1432)+24*s(1433)+24*s(1434)+24*s(1435)+32*s(1436)+48*s(1438)+16*s(1444)+16*s(1445)+16*s(1446)+16*s(1447)+16*s(1448)+48*s(1449)+192*s(1450)+8*s(1456)+8*s(1457)+8*s(1458)+8*s(1459)+96*s(1460)+16*s(1461)+8*s(1462)+8*s(1463)+8*s(1464)+4*s(1465)+20*s(1467)+256*s(1483)+32*s(1484)+120*s(1485)+4*s(1486)+8*s(1487)+8*s(1488)+32*s(1491)+4*s(1492)+4*s(1493)+4*s(1494)+16*s(1495)+8*s(1496)+8*s(1498)+8*s(1499)+8*s(1500)+8*s(1501)+4*s(1502)+4*s(1503)+4*s(1504)+12*s(1506)+2*s(1512)+2*s(1513)+2*s(1514)+2*s(1515)+4*s(1516)+12*s(1517)+24*s(1518)+4*s(1519)+12*s(1521)+4*s(1522)+4*s(1523)+4*s(1524)+4*s(1525)+4*s(1526)+4*s(1527)+6*s(1528)+6*s(1529)+6*s(1530)+8*s(1531)+12*s(1533)+4*s(1539)+4*s(1540)+4*s(1541)+4*s(1542)+4*s(1543)+12*s(1544)+48*s(1545)+2*s(1550)+2*s(1551)+2*s(1552)+2*s(1553)+24*s(1554)+4*s(1555)+2*s(1556)+2*s(1557)+2*s(1558)+8*s(1707)+30*s(1708)+1*s(1710)+2*s(1711)+2*s(1712)+1*s(1716)+1*s(1717)+1*s(1718)+4*s(1719)+2*s(1720)+2*s(1722)+2*s(1723)+2*s(1724)+2*s(1725)+1*s(1726)+1*s(1727)+1*s(1728)+3*s(1730)+1*s(1737)+1*s(1738)+1*s(1739)+1*s(1740)+1*s(1741)+3*s(1742)+12*s(1743)+1*s(1744)+2*s(1746)+1*s(1747)+1*s(1748)+1*s(1749)+1*s(1750)+1*s(1751)+1*s(1752)+3*s(1762)+1*s(1769)+1*s(1770)+1*s(1771)+1*s(1772)+1*s(1773)+3*s(1774)+12*s(1775)+3
Such that:s(1704) =< 1/2
s(1696) =< V1+3
s(1697) =< 2*V1+2
s(1699) =< V1/3+1
s(1700) =< V1/3+1/3
s(1701) =< 2/5*V1+2/5
aux(133) =< 1
aux(134) =< 2
aux(135) =< V
aux(136) =< V+1
aux(137) =< V+V1
aux(138) =< V+V1+1
aux(139) =< V+V1+2
aux(140) =< 2*V+2*V1
aux(141) =< V/2+1/2
aux(142) =< V/3+V1/3
aux(143) =< V/3+V1/3+2/3
aux(144) =< 2/5*V+2/5*V1
aux(145) =< V1
aux(146) =< V1+1
aux(147) =< V1/2+1/2
s(1322) =< aux(135)
s(1465) =< aux(139)
s(1324) =< aux(145)
s(1707) =< aux(133)
s(1708) =< aux(134)
s(1710) =< aux(145)
s(1710) =< aux(146)
s(1711) =< aux(146)
s(1712) =< aux(146)
s(1712) =< aux(134)
s(1711) =< aux(133)
s(1713) =< aux(134)* (1/2)
s(1714) =< s(1696)* (6/5)
s(1344) =< aux(146)
s(1716) =< s(1696)
s(1717) =< s(1714)
s(1718) =< s(1714)
s(1716) =< s(1714)
s(1718) =< aux(134)
s(1716) =< aux(134)
s(1719) =< aux(134)
s(1719) =< s(1713)
s(1716) =< s(1708)* (1/3)+s(1696)
s(1717) =< s(1708)* (1/5)+s(1714)
s(1718) =< s(1708)* (1/5)+s(1714)
s(1716) =< s(1708)* (1/5)+s(1714)
s(1720) =< aux(133)
s(1720) =< aux(134)
s(1721) =< aux(133)* (6/5)
s(1722) =< s(1704)
s(1723) =< aux(133)
s(1724) =< s(1721)
s(1725) =< s(1721)
s(1723) =< s(1721)
s(1725) =< aux(134)
s(1723) =< aux(134)
s(1723) =< s(1708)* (1/3)+aux(133)
s(1724) =< s(1708)* (1/5)+s(1721)
s(1725) =< s(1708)* (1/5)+s(1721)
s(1723) =< s(1708)* (1/5)+s(1721)
s(1726) =< aux(146)
s(1727) =< s(1697)
s(1728) =< s(1697)
s(1726) =< s(1697)
s(1728) =< aux(133)
s(1726) =< aux(133)
s(1726) =< s(1708)* (1/3)+aux(146)
s(1727) =< s(1708)* (1/5)+s(1697)
s(1728) =< s(1708)* (1/5)+s(1697)
s(1726) =< s(1708)* (1/5)+s(1697)
s(1729) =< aux(135)
s(1730) =< aux(135)
s(1729) =< aux(145)
s(1730) =< aux(145)
s(1729) =< s(1697)
s(1730) =< s(1697)
s(1731) =< aux(145)* (1/2)+1/2
s(1732) =< s(1730)*aux(145)
s(1733) =< s(1729)*2
s(1734) =< s(1730)*s(1731)
s(1735) =< s(1734)* (4/5)
s(1736) =< s(1734)* (2/3)
s(1737) =< s(1734)
s(1738) =< s(1736)
s(1739) =< s(1735)
s(1740) =< s(1735)
s(1738) =< s(1735)
s(1740) =< s(1729)
s(1738) =< s(1729)
s(1741) =< s(1729)
s(1742) =< s(1733)
s(1738) =< s(1742)* (1/3)+s(1736)
s(1739) =< s(1742)* (1/5)+s(1735)
s(1740) =< s(1742)* (1/5)+s(1735)
s(1738) =< s(1742)* (1/5)+s(1735)
s(1743) =< s(1732)
s(1744) =< aux(145)
s(1744) =< aux(146)
s(1744) =< aux(147)
s(1745) =< s(1699)* (6/5)
s(1746) =< aux(147)
s(1747) =< s(1699)
s(1748) =< s(1745)
s(1749) =< s(1745)
s(1747) =< s(1745)
s(1749) =< aux(134)
s(1747) =< aux(134)
s(1747) =< s(1708)* (1/3)+s(1699)
s(1748) =< s(1708)* (1/5)+s(1745)
s(1749) =< s(1708)* (1/5)+s(1745)
s(1747) =< s(1708)* (1/5)+s(1745)
s(1750) =< s(1700)
s(1751) =< s(1701)
s(1752) =< s(1701)
s(1750) =< s(1701)
s(1752) =< aux(133)
s(1750) =< aux(133)
s(1750) =< s(1708)* (1/3)+s(1700)
s(1751) =< s(1708)* (1/5)+s(1701)
s(1752) =< s(1708)* (1/5)+s(1701)
s(1750) =< s(1708)* (1/5)+s(1701)
s(1761) =< aux(135)
s(1762) =< aux(135)
s(1761) =< aux(145)
s(1762) =< aux(145)
s(1764) =< s(1762)*aux(145)
s(1765) =< s(1761)*2
s(1766) =< s(1762)*s(1731)
s(1767) =< s(1766)* (4/5)
s(1768) =< s(1766)* (2/3)
s(1769) =< s(1766)
s(1770) =< s(1768)
s(1771) =< s(1767)
s(1772) =< s(1767)
s(1770) =< s(1767)
s(1772) =< s(1761)
s(1770) =< s(1761)
s(1773) =< s(1761)
s(1774) =< s(1765)
s(1770) =< s(1774)* (1/3)+s(1768)
s(1771) =< s(1774)* (1/5)+s(1767)
s(1772) =< s(1774)* (1/5)+s(1767)
s(1770) =< s(1774)* (1/5)+s(1767)
s(1775) =< s(1764)
s(1341) =< aux(135)
s(1341) =< aux(136)
s(1342) =< aux(136)
s(1343) =< aux(136)
s(1341) =< aux(141)
s(1343) =< aux(146)
s(1342) =< aux(147)
s(1345) =< aux(146)* (1/2)
s(1346) =< aux(143)* (6/5)
s(1347) =< aux(141)
s(1348) =< aux(143)
s(1349) =< s(1346)
s(1350) =< s(1346)
s(1348) =< s(1346)
s(1350) =< aux(146)
s(1348) =< aux(146)
s(1351) =< aux(146)
s(1351) =< s(1345)
s(1348) =< s(1344)* (1/3)+aux(143)
s(1349) =< s(1344)* (1/5)+s(1346)
s(1350) =< s(1344)* (1/5)+s(1346)
s(1348) =< s(1344)* (1/5)+s(1346)
s(1353) =< aux(142)
s(1354) =< aux(144)
s(1355) =< aux(144)
s(1353) =< aux(144)
s(1355) =< aux(145)
s(1353) =< aux(145)
s(1356) =< aux(145)
s(1356) =< aux(147)
s(1353) =< s(1344)* (1/3)+aux(142)
s(1354) =< s(1344)* (1/5)+aux(144)
s(1355) =< s(1344)* (1/5)+aux(144)
s(1353) =< s(1344)* (1/5)+aux(144)
s(1357) =< aux(137)
s(1358) =< aux(137)
s(1358) =< aux(138)
s(1359) =< aux(138)
s(1360) =< aux(138)* (1/2)
s(1361) =< aux(139)* (6/5)
s(1362) =< aux(139)
s(1363) =< s(1361)
s(1364) =< s(1361)
s(1362) =< s(1361)
s(1364) =< aux(138)
s(1362) =< aux(138)
s(1365) =< aux(138)
s(1365) =< s(1360)
s(1362) =< s(1359)* (1/3)+aux(139)
s(1363) =< s(1359)* (1/5)+s(1361)
s(1364) =< s(1359)* (1/5)+s(1361)
s(1362) =< s(1359)* (1/5)+s(1361)
s(1366) =< aux(137)
s(1367) =< aux(140)
s(1368) =< aux(140)
s(1366) =< aux(140)
s(1368) =< aux(137)
s(1366) =< s(1359)* (1/3)+aux(137)
s(1367) =< s(1359)* (1/5)+aux(140)
s(1368) =< s(1359)* (1/5)+aux(140)
s(1366) =< s(1359)* (1/5)+aux(140)
s(1369) =< aux(137)+1
s(1370) =< aux(137)
s(1371) =< aux(142)
s(1372) =< aux(137)+3
s(1373) =< aux(137)* (1/2)+1/2
s(1374) =< aux(137)* (1/2)
s(1375) =< aux(137)*2
s(1376) =< s(1357)*aux(142)
s(1377) =< s(1357)*s(1369)
s(1378) =< s(1357)*s(1370)
s(1379) =< s(1357)*s(1371)
s(1380) =< s(1357)*s(1372)
s(1381) =< s(1376)* (6/5)
s(1382) =< s(1357)*s(1373)
s(1383) =< s(1377)* (1/2)
s(1384) =< s(1379)* (6/5)
s(1385) =< s(1377)* (2/5)
s(1386) =< s(1377)* (1/3)
s(1387) =< s(1380)* (1/3)
s(1388) =< s(1377)*2
s(1389) =< s(1378)
s(1390) =< s(1375)
s(1391) =< s(1378)
s(1391) =< s(1377)
s(1392) =< s(1377)
s(1393) =< s(1377)
s(1393) =< s(1375)
s(1392) =< aux(137)
s(1394) =< s(1375)* (1/2)
s(1395) =< s(1380)* (6/5)
s(1396) =< s(1377)
s(1397) =< s(1380)
s(1398) =< s(1395)
s(1399) =< s(1395)
s(1397) =< s(1395)
s(1399) =< s(1375)
s(1397) =< s(1375)
s(1400) =< s(1375)
s(1400) =< s(1394)
s(1397) =< s(1390)* (1/3)+s(1380)
s(1398) =< s(1390)* (1/5)+s(1395)
s(1399) =< s(1390)* (1/5)+s(1395)
s(1397) =< s(1390)* (1/5)+s(1395)
s(1401) =< aux(137)
s(1401) =< s(1375)
s(1402) =< aux(137)* (6/5)
s(1403) =< s(1374)
s(1404) =< aux(137)
s(1405) =< s(1402)
s(1406) =< s(1402)
s(1404) =< s(1402)
s(1406) =< s(1375)
s(1404) =< s(1375)
s(1404) =< s(1390)* (1/3)+aux(137)
s(1405) =< s(1390)* (1/5)+s(1402)
s(1406) =< s(1390)* (1/5)+s(1402)
s(1404) =< s(1390)* (1/5)+s(1402)
s(1407) =< s(1377)
s(1408) =< s(1388)
s(1409) =< s(1388)
s(1407) =< s(1388)
s(1409) =< aux(137)
s(1407) =< aux(137)
s(1407) =< s(1390)* (1/3)+s(1377)
s(1408) =< s(1390)* (1/5)+s(1388)
s(1409) =< s(1390)* (1/5)+s(1388)
s(1407) =< s(1390)* (1/5)+s(1388)
s(1410) =< s(1378)
s(1411) =< s(1378)
s(1410) =< s(1388)
s(1411) =< s(1388)
s(1412) =< s(1411)*aux(137)
s(1413) =< s(1410)*2
s(1414) =< s(1411)*s(1373)
s(1415) =< s(1414)* (4/5)
s(1416) =< s(1414)* (2/3)
s(1417) =< s(1414)
s(1418) =< s(1416)
s(1419) =< s(1415)
s(1420) =< s(1415)
s(1418) =< s(1415)
s(1420) =< s(1410)
s(1418) =< s(1410)
s(1421) =< s(1410)
s(1422) =< s(1413)
s(1418) =< s(1422)* (1/3)+s(1416)
s(1419) =< s(1422)* (1/5)+s(1415)
s(1420) =< s(1422)* (1/5)+s(1415)
s(1418) =< s(1422)* (1/5)+s(1415)
s(1423) =< s(1412)
s(1424) =< s(1378)
s(1424) =< s(1377)
s(1424) =< s(1383)
s(1425) =< s(1387)* (6/5)
s(1426) =< s(1383)
s(1427) =< s(1387)
s(1428) =< s(1425)
s(1429) =< s(1425)
s(1427) =< s(1425)
s(1429) =< s(1375)
s(1427) =< s(1375)
s(1427) =< s(1390)* (1/3)+s(1387)
s(1428) =< s(1390)* (1/5)+s(1425)
s(1429) =< s(1390)* (1/5)+s(1425)
s(1427) =< s(1390)* (1/5)+s(1425)
s(1430) =< s(1386)
s(1431) =< s(1385)
s(1432) =< s(1385)
s(1430) =< s(1385)
s(1432) =< aux(137)
s(1430) =< aux(137)
s(1430) =< s(1390)* (1/3)+s(1386)
s(1431) =< s(1390)* (1/5)+s(1385)
s(1432) =< s(1390)* (1/5)+s(1385)
s(1430) =< s(1390)* (1/5)+s(1385)
s(1433) =< s(1379)
s(1434) =< s(1384)
s(1435) =< s(1384)
s(1433) =< s(1384)
s(1435) =< s(1378)
s(1433) =< s(1378)
s(1436) =< s(1378)
s(1436) =< s(1383)
s(1433) =< s(1396)* (1/3)+s(1379)
s(1434) =< s(1396)* (1/5)+s(1384)
s(1435) =< s(1396)* (1/5)+s(1384)
s(1433) =< s(1396)* (1/5)+s(1384)
s(1437) =< s(1378)
s(1438) =< s(1378)
s(1437) =< aux(137)
s(1438) =< aux(137)
s(1439) =< s(1438)*aux(137)
s(1440) =< s(1437)*2
s(1441) =< s(1438)*s(1373)
s(1442) =< s(1441)* (4/5)
s(1443) =< s(1441)* (2/3)
s(1444) =< s(1441)
s(1445) =< s(1443)
s(1446) =< s(1442)
s(1447) =< s(1442)
s(1445) =< s(1442)
s(1447) =< s(1437)
s(1445) =< s(1437)
s(1448) =< s(1437)
s(1449) =< s(1440)
s(1445) =< s(1449)* (1/3)+s(1443)
s(1446) =< s(1449)* (1/5)+s(1442)
s(1447) =< s(1449)* (1/5)+s(1442)
s(1445) =< s(1449)* (1/5)+s(1442)
s(1450) =< s(1439)
s(1451) =< s(1370)* (1/2)+1/2
s(1452) =< s(1411)*s(1370)
s(1453) =< s(1411)*s(1451)
s(1454) =< s(1453)* (4/5)
s(1455) =< s(1453)* (2/3)
s(1456) =< s(1453)
s(1457) =< s(1455)
s(1458) =< s(1454)
s(1459) =< s(1454)
s(1457) =< s(1454)
s(1459) =< s(1410)
s(1457) =< s(1410)
s(1457) =< s(1422)* (1/3)+s(1455)
s(1458) =< s(1422)* (1/5)+s(1454)
s(1459) =< s(1422)* (1/5)+s(1454)
s(1457) =< s(1422)* (1/5)+s(1454)
s(1460) =< s(1452)
s(1461) =< s(1382)
s(1462) =< s(1376)
s(1463) =< s(1381)
s(1464) =< s(1381)
s(1462) =< s(1381)
s(1464) =< s(1378)
s(1462) =< s(1378)
s(1462) =< s(1396)* (1/3)+s(1376)
s(1463) =< s(1396)* (1/5)+s(1381)
s(1464) =< s(1396)* (1/5)+s(1381)
s(1462) =< s(1396)* (1/5)+s(1381)
s(1466) =< aux(137)
s(1467) =< aux(137)
s(1466) =< aux(139)
s(1467) =< aux(139)
s(1468) =< s(1466)* (1/2)
s(1469) =< s(1466)*2
s(1470) =< s(1467)*aux(142)
s(1471) =< s(1467)*s(1369)
s(1472) =< s(1467)*s(1370)
s(1473) =< s(1467)*s(1371)
s(1474) =< s(1467)*s(1372)
s(1475) =< s(1470)* (6/5)
s(1476) =< s(1467)*s(1373)
s(1477) =< s(1471)* (1/2)
s(1478) =< s(1473)* (6/5)
s(1479) =< s(1471)* (2/5)
s(1480) =< s(1471)* (1/3)
s(1481) =< s(1474)* (1/3)
s(1482) =< s(1471)*2
s(1483) =< s(1472)
s(1484) =< s(1466)
s(1485) =< s(1469)
s(1486) =< s(1472)
s(1486) =< s(1471)
s(1487) =< s(1471)
s(1488) =< s(1471)
s(1488) =< s(1469)
s(1487) =< s(1466)
s(1489) =< s(1469)* (1/2)
s(1490) =< s(1474)* (6/5)
s(1491) =< s(1471)
s(1492) =< s(1474)
s(1493) =< s(1490)
s(1494) =< s(1490)
s(1492) =< s(1490)
s(1494) =< s(1469)
s(1492) =< s(1469)
s(1495) =< s(1469)
s(1495) =< s(1489)
s(1492) =< s(1485)* (1/3)+s(1474)
s(1493) =< s(1485)* (1/5)+s(1490)
s(1494) =< s(1485)* (1/5)+s(1490)
s(1492) =< s(1485)* (1/5)+s(1490)
s(1496) =< s(1466)
s(1496) =< s(1469)
s(1497) =< s(1466)* (6/5)
s(1498) =< s(1468)
s(1499) =< s(1466)
s(1500) =< s(1497)
s(1501) =< s(1497)
s(1499) =< s(1497)
s(1501) =< s(1469)
s(1499) =< s(1469)
s(1499) =< s(1485)* (1/3)+s(1466)
s(1500) =< s(1485)* (1/5)+s(1497)
s(1501) =< s(1485)* (1/5)+s(1497)
s(1499) =< s(1485)* (1/5)+s(1497)
s(1502) =< s(1471)
s(1503) =< s(1482)
s(1504) =< s(1482)
s(1502) =< s(1482)
s(1504) =< s(1466)
s(1502) =< s(1466)
s(1502) =< s(1485)* (1/3)+s(1471)
s(1503) =< s(1485)* (1/5)+s(1482)
s(1504) =< s(1485)* (1/5)+s(1482)
s(1502) =< s(1485)* (1/5)+s(1482)
s(1505) =< s(1472)
s(1506) =< s(1472)
s(1505) =< s(1482)
s(1506) =< s(1482)
s(1507) =< s(1506)*aux(137)
s(1508) =< s(1505)*2
s(1509) =< s(1506)*s(1373)
s(1510) =< s(1509)* (4/5)
s(1511) =< s(1509)* (2/3)
s(1512) =< s(1509)
s(1513) =< s(1511)
s(1514) =< s(1510)
s(1515) =< s(1510)
s(1513) =< s(1510)
s(1515) =< s(1505)
s(1513) =< s(1505)
s(1516) =< s(1505)
s(1517) =< s(1508)
s(1513) =< s(1517)* (1/3)+s(1511)
s(1514) =< s(1517)* (1/5)+s(1510)
s(1515) =< s(1517)* (1/5)+s(1510)
s(1513) =< s(1517)* (1/5)+s(1510)
s(1518) =< s(1507)
s(1519) =< s(1472)
s(1519) =< s(1471)
s(1519) =< s(1477)
s(1520) =< s(1481)* (6/5)
s(1521) =< s(1477)
s(1522) =< s(1481)
s(1523) =< s(1520)
s(1524) =< s(1520)
s(1522) =< s(1520)
s(1524) =< s(1469)
s(1522) =< s(1469)
s(1522) =< s(1485)* (1/3)+s(1481)
s(1523) =< s(1485)* (1/5)+s(1520)
s(1524) =< s(1485)* (1/5)+s(1520)
s(1522) =< s(1485)* (1/5)+s(1520)
s(1525) =< s(1480)
s(1526) =< s(1479)
s(1527) =< s(1479)
s(1525) =< s(1479)
s(1527) =< s(1466)
s(1525) =< s(1466)
s(1525) =< s(1485)* (1/3)+s(1480)
s(1526) =< s(1485)* (1/5)+s(1479)
s(1527) =< s(1485)* (1/5)+s(1479)
s(1525) =< s(1485)* (1/5)+s(1479)
s(1528) =< s(1473)
s(1529) =< s(1478)
s(1530) =< s(1478)
s(1528) =< s(1478)
s(1530) =< s(1472)
s(1528) =< s(1472)
s(1531) =< s(1472)
s(1531) =< s(1477)
s(1528) =< s(1491)* (1/3)+s(1473)
s(1529) =< s(1491)* (1/5)+s(1478)
s(1530) =< s(1491)* (1/5)+s(1478)
s(1528) =< s(1491)* (1/5)+s(1478)
s(1532) =< s(1472)
s(1533) =< s(1472)
s(1532) =< s(1466)
s(1533) =< s(1466)
s(1534) =< s(1533)*aux(137)
s(1535) =< s(1532)*2
s(1536) =< s(1533)*s(1373)
s(1537) =< s(1536)* (4/5)
s(1538) =< s(1536)* (2/3)
s(1539) =< s(1536)
s(1540) =< s(1538)
s(1541) =< s(1537)
s(1542) =< s(1537)
s(1540) =< s(1537)
s(1542) =< s(1532)
s(1540) =< s(1532)
s(1543) =< s(1532)
s(1544) =< s(1535)
s(1540) =< s(1544)* (1/3)+s(1538)
s(1541) =< s(1544)* (1/5)+s(1537)
s(1542) =< s(1544)* (1/5)+s(1537)
s(1540) =< s(1544)* (1/5)+s(1537)
s(1545) =< s(1534)
s(1546) =< s(1506)*s(1370)
s(1547) =< s(1506)*s(1451)
s(1548) =< s(1547)* (4/5)
s(1549) =< s(1547)* (2/3)
s(1550) =< s(1547)
s(1551) =< s(1549)
s(1552) =< s(1548)
s(1553) =< s(1548)
s(1551) =< s(1548)
s(1553) =< s(1505)
s(1551) =< s(1505)
s(1551) =< s(1517)* (1/3)+s(1549)
s(1552) =< s(1517)* (1/5)+s(1548)
s(1553) =< s(1517)* (1/5)+s(1548)
s(1551) =< s(1517)* (1/5)+s(1548)
s(1554) =< s(1546)
s(1555) =< s(1476)
s(1556) =< s(1470)
s(1557) =< s(1475)
s(1558) =< s(1475)
s(1556) =< s(1475)
s(1558) =< s(1472)
s(1556) =< s(1472)
s(1556) =< s(1491)* (1/3)+s(1470)
s(1557) =< s(1491)* (1/5)+s(1475)
s(1558) =< s(1491)* (1/5)+s(1475)
s(1556) =< s(1491)* (1/5)+s(1475)
with precondition: [V>=0]
* Chain [73]: 329*s(2112)+127*s(2128)+197*s(2129)+9*s(2131)+5*s(2132)+4*s(2133)+40*s(2136)+2*s(2137)+2*s(2138)+2*s(2139)+24*s(2140)+14*s(2141)+29*s(2143)+13*s(2144)+13*s(2145)+13*s(2146)+2*s(2147)+2*s(2148)+2*s(2149)+6*s(2151)+2*s(2158)+2*s(2159)+2*s(2160)+2*s(2161)+2*s(2162)+6*s(2163)+24*s(2164)+4*s(2165)+14*s(2167)+2*s(2168)+2*s(2169)+2*s(2170)+2*s(2171)+2*s(2172)+2*s(2173)+1*s(2189)+1*s(2195)+1*s(2196)+1*s(2197)+3*s(2198)+4*s(2201)+1*s(2209)+1*s(2210)+1*s(2211)+1*s(2212)+4*s(2213)+4*s(2214)+4*s(2215)+384*s(2236)+180*s(2237)+6*s(2238)+12*s(2239)+12*s(2240)+48*s(2243)+6*s(2244)+6*s(2245)+6*s(2246)+24*s(2247)+12*s(2248)+12*s(2250)+12*s(2251)+12*s(2252)+12*s(2253)+6*s(2254)+6*s(2255)+6*s(2256)+18*s(2258)+3*s(2264)+3*s(2265)+3*s(2266)+3*s(2267)+6*s(2268)+18*s(2269)+36*s(2270)+6*s(2271)+18*s(2273)+6*s(2274)+6*s(2275)+6*s(2276)+6*s(2277)+6*s(2278)+6*s(2279)+9*s(2280)+9*s(2281)+9*s(2282)+12*s(2283)+18*s(2285)+6*s(2291)+6*s(2292)+6*s(2293)+6*s(2294)+6*s(2295)+18*s(2296)+72*s(2297)+3*s(2303)+3*s(2304)+3*s(2305)+3*s(2306)+36*s(2307)+6*s(2308)+3*s(2309)+3*s(2310)+3*s(2311)+1*s(2312)+10*s(2314)+128*s(2330)+16*s(2331)+60*s(2332)+2*s(2333)+4*s(2334)+4*s(2335)+16*s(2338)+2*s(2339)+2*s(2340)+2*s(2341)+8*s(2342)+4*s(2343)+4*s(2345)+4*s(2346)+4*s(2347)+4*s(2348)+2*s(2349)+2*s(2350)+2*s(2351)+6*s(2353)+1*s(2359)+1*s(2360)+1*s(2361)+1*s(2362)+2*s(2363)+6*s(2364)+12*s(2365)+2*s(2366)+6*s(2368)+2*s(2369)+2*s(2370)+2*s(2371)+2*s(2372)+2*s(2373)+2*s(2374)+3*s(2375)+3*s(2376)+3*s(2377)+4*s(2378)+6*s(2380)+2*s(2386)+2*s(2387)+2*s(2388)+2*s(2389)+2*s(2390)+6*s(2391)+24*s(2392)+1*s(2397)+1*s(2398)+1*s(2399)+1*s(2400)+12*s(2401)+2*s(2402)+1*s(2403)+1*s(2404)+1*s(2405)+15*s(2475)+2*s(2482)+2*s(2483)+2*s(2484)+2*s(2485)+5*s(2486)+15*s(2487)+24*s(2488)+4*s(2504)+141*s(2506)+3*s(2510)+3*s(2511)+3*s(2512)+7*s(2513)+381*s(2514)+12*s(2515)+12*s(2516)+12*s(2517)+16*s(2518)+304*s(2519)+15*s(2520)+72*s(2521)+3*s(2524)+3*s(2525)+3*s(2526)+3*s(2527)+12*s(2528)+12*s(2529)+12*s(2530)+1408*s(2551)+660*s(2552)+22*s(2553)+44*s(2554)+44*s(2555)+176*s(2558)+22*s(2559)+22*s(2560)+22*s(2561)+88*s(2562)+44*s(2563)+44*s(2565)+44*s(2566)+44*s(2567)+44*s(2568)+22*s(2569)+22*s(2570)+22*s(2571)+66*s(2573)+11*s(2579)+11*s(2580)+11*s(2581)+11*s(2582)+22*s(2583)+66*s(2584)+132*s(2585)+22*s(2586)+66*s(2588)+22*s(2589)+22*s(2590)+22*s(2591)+22*s(2592)+22*s(2593)+22*s(2594)+33*s(2595)+33*s(2596)+33*s(2597)+44*s(2598)+66*s(2600)+22*s(2606)+22*s(2607)+22*s(2608)+22*s(2609)+22*s(2610)+66*s(2611)+264*s(2612)+11*s(2618)+11*s(2619)+11*s(2620)+11*s(2621)+132*s(2622)+22*s(2623)+11*s(2624)+11*s(2625)+11*s(2626)+6*s(2627)+40*s(2629)+512*s(2645)+64*s(2646)+240*s(2647)+8*s(2648)+16*s(2649)+16*s(2650)+64*s(2653)+8*s(2654)+8*s(2655)+8*s(2656)+32*s(2657)+16*s(2658)+16*s(2660)+16*s(2661)+16*s(2662)+16*s(2663)+8*s(2664)+8*s(2665)+8*s(2666)+24*s(2668)+4*s(2674)+4*s(2675)+4*s(2676)+4*s(2677)+8*s(2678)+24*s(2679)+48*s(2680)+8*s(2681)+24*s(2683)+8*s(2684)+8*s(2685)+8*s(2686)+8*s(2687)+8*s(2688)+8*s(2689)+12*s(2690)+12*s(2691)+12*s(2692)+16*s(2693)+24*s(2695)+8*s(2701)+8*s(2702)+8*s(2703)+8*s(2704)+8*s(2705)+24*s(2706)+96*s(2707)+4*s(2712)+4*s(2713)+4*s(2714)+4*s(2715)+48*s(2716)+8*s(2717)+4*s(2718)+4*s(2719)+4*s(2720)+6*s(2731)+2*s(2738)+2*s(2739)+2*s(2740)+2*s(2741)+2*s(2742)+6*s(2743)+24*s(2744)+6*s(2755)+2*s(2762)+2*s(2763)+2*s(2764)+2*s(2765)+2*s(2766)+6*s(2767)+24*s(2768)+1*s(2946)+1*s(2947)+1*s(2948)+1*s(2956)+1*s(2957)+1*s(2958)+1*s(2980)+1*s(2981)+1*s(2982)+1*s(2998)+1*s(3004)+1*s(3005)+1*s(3006)+1*s(3018)+1*s(3019)+1*s(3020)+6*s(3232)+4*s(3233)+2*s(3237)+2*s(3238)+2*s(3239)+2*s(3247)+2*s(3248)+2*s(3249)+6*s(3251)+2*s(3258)+2*s(3259)+2*s(3260)+2*s(3261)+2*s(3262)+6*s(3263)+24*s(3264)+2*s(3265)+4*s(3267)+2*s(3268)+2*s(3269)+2*s(3270)+2*s(3271)+2*s(3272)+2*s(3273)+2*s(3289)+2*s(3295)+2*s(3296)+2*s(3297)+8*s(3300)+8*s(3301)+8*s(3302)+16*s(3303)+2*s(3309)+2*s(3310)+2*s(3311)+8*s(3313)+8*s(3314)+8*s(3315)+768*s(3336)+360*s(3337)+12*s(3338)+24*s(3339)+24*s(3340)+96*s(3343)+12*s(3344)+12*s(3345)+12*s(3346)+48*s(3347)+24*s(3348)+24*s(3350)+24*s(3351)+24*s(3352)+24*s(3353)+12*s(3354)+12*s(3355)+12*s(3356)+36*s(3358)+6*s(3364)+6*s(3365)+6*s(3366)+6*s(3367)+12*s(3368)+36*s(3369)+72*s(3370)+12*s(3371)+36*s(3373)+12*s(3374)+12*s(3375)+12*s(3376)+12*s(3377)+12*s(3378)+12*s(3379)+18*s(3380)+18*s(3381)+18*s(3382)+24*s(3383)+36*s(3385)+12*s(3391)+12*s(3392)+12*s(3393)+12*s(3394)+12*s(3395)+36*s(3396)+144*s(3397)+6*s(3403)+6*s(3404)+6*s(3405)+6*s(3406)+72*s(3407)+12*s(3408)+6*s(3409)+6*s(3410)+6*s(3411)+2*s(3412)+20*s(3414)+256*s(3430)+32*s(3431)+120*s(3432)+4*s(3433)+8*s(3434)+8*s(3435)+32*s(3438)+4*s(3439)+4*s(3440)+4*s(3441)+16*s(3442)+8*s(3443)+8*s(3445)+8*s(3446)+8*s(3447)+8*s(3448)+4*s(3449)+4*s(3450)+4*s(3451)+12*s(3453)+2*s(3459)+2*s(3460)+2*s(3461)+2*s(3462)+4*s(3463)+12*s(3464)+24*s(3465)+4*s(3466)+12*s(3468)+4*s(3469)+4*s(3470)+4*s(3471)+4*s(3472)+4*s(3473)+4*s(3474)+6*s(3475)+6*s(3476)+6*s(3477)+8*s(3478)+12*s(3480)+4*s(3486)+4*s(3487)+4*s(3488)+4*s(3489)+4*s(3490)+12*s(3491)+48*s(3492)+2*s(3497)+2*s(3498)+2*s(3499)+2*s(3500)+24*s(3501)+4*s(3502)+2*s(3503)+2*s(3504)+2*s(3505)+3*s(3523)+3*s(3524)+3*s(3525)+3*s(3526)+36*s(3529)+2*s(3545)+12*s(3772)+4*s(3779)+4*s(3780)+4*s(3781)+4*s(3782)+4*s(3783)+12*s(3784)+48*s(3785)+3*s(4546)+1*s(4553)+1*s(4554)+1*s(4555)+1*s(4556)+1*s(4557)+3*s(4558)+12*s(4559)+2*s(4680)+2*s(4681)+1*s(4685)+1*s(4686)+1*s(4687)+1*s(4695)+1*s(4696)+1*s(4697)+3*s(4699)+1*s(4706)+1*s(4707)+1*s(4708)+1*s(4709)+1*s(4710)+3*s(4711)+12*s(4712)+1*s(4713)+2*s(4715)+1*s(4716)+1*s(4717)+1*s(4718)+1*s(4719)+1*s(4720)+1*s(4721)+6
Such that:s(2926) =< 3
s(2930) =< 1/3
s(2988) =< 2/3
s(2931) =< 2/5
s(4667) =< V35/2
aux(205) =< 1
aux(206) =< 2
aux(207) =< 1/2
aux(208) =< -V1+V35
aux(209) =< V1
aux(210) =< V1+1
aux(211) =< V1+2
aux(212) =< V1+3
aux(213) =< V1-V35
aux(214) =< V1+V35
aux(215) =< V1+V35+1
aux(216) =< V1+V35+2
aux(217) =< 2*V1
aux(218) =< 2*V1+2
aux(219) =< 2*V1+2*V35
aux(220) =< V1/2+1/2
aux(221) =< V1/3
aux(222) =< V1/3+1
aux(223) =< V1/3+1/3
aux(224) =< V1/3+2/3
aux(225) =< 2/5*V1
aux(226) =< 2/5*V1+2/5
aux(227) =< V35
aux(228) =< V35+1
aux(229) =< V35+2
aux(230) =< V35+3
aux(231) =< 2*V35
aux(232) =< 2*V35+2
aux(233) =< V35/2+1/2
aux(234) =< V35/3
aux(235) =< V35/3+1
aux(236) =< V35/3+1/3
aux(237) =< V35/3+2/3
aux(238) =< 2/5*V35
aux(239) =< 2/5*V35+2/5
s(2506) =< aux(210)
s(2627) =< aux(216)
s(2112) =< aux(227)
s(2136) =< aux(228)
s(2128) =< aux(205)
s(2129) =< aux(206)
s(2131) =< aux(227)
s(2131) =< aux(228)
s(2132) =< aux(228)
s(2133) =< aux(228)
s(2133) =< aux(206)
s(2132) =< aux(205)
s(2134) =< aux(206)* (1/2)
s(2135) =< aux(230)* (6/5)
s(2137) =< aux(230)
s(2138) =< s(2135)
s(2139) =< s(2135)
s(2137) =< s(2135)
s(2139) =< aux(206)
s(2137) =< aux(206)
s(2140) =< aux(206)
s(2140) =< s(2134)
s(2137) =< s(2129)* (1/3)+aux(230)
s(2138) =< s(2129)* (1/5)+s(2135)
s(2139) =< s(2129)* (1/5)+s(2135)
s(2137) =< s(2129)* (1/5)+s(2135)
s(2141) =< aux(205)
s(2141) =< aux(206)
s(2142) =< aux(205)* (6/5)
s(2143) =< aux(207)
s(2144) =< aux(205)
s(2145) =< s(2142)
s(2146) =< s(2142)
s(2144) =< s(2142)
s(2146) =< aux(206)
s(2144) =< aux(206)
s(2144) =< s(2129)* (1/3)+aux(205)
s(2145) =< s(2129)* (1/5)+s(2142)
s(2146) =< s(2129)* (1/5)+s(2142)
s(2144) =< s(2129)* (1/5)+s(2142)
s(2147) =< aux(228)
s(2148) =< aux(232)
s(2149) =< aux(232)
s(2147) =< aux(232)
s(2149) =< aux(205)
s(2147) =< aux(205)
s(2147) =< s(2129)* (1/3)+aux(228)
s(2148) =< s(2129)* (1/5)+aux(232)
s(2149) =< s(2129)* (1/5)+aux(232)
s(2147) =< s(2129)* (1/5)+aux(232)
s(2150) =< aux(209)
s(2151) =< aux(209)
s(2150) =< aux(227)
s(2151) =< aux(227)
s(2150) =< aux(232)
s(2151) =< aux(232)
s(2152) =< aux(227)* (1/2)+1/2
s(2153) =< s(2151)*aux(227)
s(2154) =< s(2150)*2
s(2155) =< s(2151)*s(2152)
s(2156) =< s(2155)* (4/5)
s(2157) =< s(2155)* (2/3)
s(2158) =< s(2155)
s(2159) =< s(2157)
s(2160) =< s(2156)
s(2161) =< s(2156)
s(2159) =< s(2156)
s(2161) =< s(2150)
s(2159) =< s(2150)
s(2162) =< s(2150)
s(2163) =< s(2154)
s(2159) =< s(2163)* (1/3)+s(2157)
s(2160) =< s(2163)* (1/5)+s(2156)
s(2161) =< s(2163)* (1/5)+s(2156)
s(2159) =< s(2163)* (1/5)+s(2156)
s(2164) =< s(2153)
s(2165) =< aux(227)
s(2165) =< aux(228)
s(2165) =< aux(233)
s(2166) =< aux(235)* (6/5)
s(2167) =< aux(233)
s(2168) =< aux(235)
s(2169) =< s(2166)
s(2170) =< s(2166)
s(2168) =< s(2166)
s(2170) =< aux(206)
s(2168) =< aux(206)
s(2168) =< s(2129)* (1/3)+aux(235)
s(2169) =< s(2129)* (1/5)+s(2166)
s(2170) =< s(2129)* (1/5)+s(2166)
s(2168) =< s(2129)* (1/5)+s(2166)
s(2171) =< aux(236)
s(2172) =< aux(239)
s(2173) =< aux(239)
s(2171) =< aux(239)
s(2173) =< aux(205)
s(2171) =< aux(205)
s(2171) =< s(2129)* (1/3)+aux(236)
s(2172) =< s(2129)* (1/5)+aux(239)
s(2173) =< s(2129)* (1/5)+aux(239)
s(2171) =< s(2129)* (1/5)+aux(239)
s(2504) =< aux(228)
s(2504) =< aux(210)
s(2507) =< aux(210)* (1/2)
s(2508) =< aux(216)* (6/5)
s(2510) =< aux(216)
s(2511) =< s(2508)
s(2512) =< s(2508)
s(2510) =< s(2508)
s(2512) =< aux(210)
s(2510) =< aux(210)
s(2513) =< aux(210)
s(2513) =< s(2507)
s(2510) =< s(2506)* (1/3)+aux(216)
s(2511) =< s(2506)* (1/5)+s(2508)
s(2512) =< s(2506)* (1/5)+s(2508)
s(2510) =< s(2506)* (1/5)+s(2508)
s(2514) =< aux(209)
s(2515) =< aux(214)
s(2516) =< aux(219)
s(2517) =< aux(219)
s(2515) =< aux(219)
s(2517) =< aux(209)
s(2515) =< aux(209)
s(2518) =< aux(209)
s(2518) =< aux(210)
s(2515) =< s(2506)* (1/3)+aux(214)
s(2516) =< s(2506)* (1/5)+aux(219)
s(2517) =< s(2506)* (1/5)+aux(219)
s(2515) =< s(2506)* (1/5)+aux(219)
s(2519) =< aux(214)
s(2520) =< aux(214)
s(2520) =< aux(215)
s(2521) =< aux(215)
s(2522) =< aux(215)* (1/2)
s(2524) =< aux(216)
s(2525) =< s(2508)
s(2526) =< s(2508)
s(2524) =< s(2508)
s(2526) =< aux(215)
s(2524) =< aux(215)
s(2527) =< aux(215)
s(2527) =< s(2522)
s(2524) =< s(2521)* (1/3)+aux(216)
s(2525) =< s(2521)* (1/5)+s(2508)
s(2526) =< s(2521)* (1/5)+s(2508)
s(2524) =< s(2521)* (1/5)+s(2508)
s(2528) =< aux(214)
s(2529) =< aux(219)
s(2530) =< aux(219)
s(2528) =< aux(219)
s(2530) =< aux(214)
s(2528) =< s(2521)* (1/3)+aux(214)
s(2529) =< s(2521)* (1/5)+aux(219)
s(2530) =< s(2521)* (1/5)+aux(219)
s(2528) =< s(2521)* (1/5)+aux(219)
s(2531) =< aux(214)+1
s(2532) =< aux(214)
s(2534) =< aux(214)+3
s(2535) =< aux(214)* (1/2)+1/2
s(2536) =< aux(214)* (1/2)
s(2537) =< aux(214)*2
s(2538) =< s(2519)*aux(214)
s(2539) =< s(2519)*s(2531)
s(2540) =< s(2519)*s(2532)
s(2542) =< s(2519)*s(2534)
s(2543) =< s(2538)* (6/5)
s(2544) =< s(2519)*s(2535)
s(2545) =< s(2539)* (1/2)
s(2546) =< s(2540)* (6/5)
s(2547) =< s(2539)* (2/5)
s(2548) =< s(2539)* (1/3)
s(2549) =< s(2542)* (1/3)
s(2550) =< s(2539)*2
s(2551) =< s(2540)
s(2552) =< s(2537)
s(2553) =< s(2540)
s(2553) =< s(2539)
s(2554) =< s(2539)
s(2555) =< s(2539)
s(2555) =< s(2537)
s(2554) =< aux(214)
s(2556) =< s(2537)* (1/2)
s(2557) =< s(2542)* (6/5)
s(2558) =< s(2539)
s(2559) =< s(2542)
s(2560) =< s(2557)
s(2561) =< s(2557)
s(2559) =< s(2557)
s(2561) =< s(2537)
s(2559) =< s(2537)
s(2562) =< s(2537)
s(2562) =< s(2556)
s(2559) =< s(2552)* (1/3)+s(2542)
s(2560) =< s(2552)* (1/5)+s(2557)
s(2561) =< s(2552)* (1/5)+s(2557)
s(2559) =< s(2552)* (1/5)+s(2557)
s(2563) =< aux(214)
s(2563) =< s(2537)
s(2564) =< aux(214)* (6/5)
s(2565) =< s(2536)
s(2566) =< aux(214)
s(2567) =< s(2564)
s(2568) =< s(2564)
s(2566) =< s(2564)
s(2568) =< s(2537)
s(2566) =< s(2537)
s(2566) =< s(2552)* (1/3)+aux(214)
s(2567) =< s(2552)* (1/5)+s(2564)
s(2568) =< s(2552)* (1/5)+s(2564)
s(2566) =< s(2552)* (1/5)+s(2564)
s(2569) =< s(2539)
s(2570) =< s(2550)
s(2571) =< s(2550)
s(2569) =< s(2550)
s(2571) =< aux(214)
s(2569) =< aux(214)
s(2569) =< s(2552)* (1/3)+s(2539)
s(2570) =< s(2552)* (1/5)+s(2550)
s(2571) =< s(2552)* (1/5)+s(2550)
s(2569) =< s(2552)* (1/5)+s(2550)
s(2572) =< s(2540)
s(2573) =< s(2540)
s(2572) =< s(2550)
s(2573) =< s(2550)
s(2574) =< s(2573)*aux(214)
s(2575) =< s(2572)*2
s(2576) =< s(2573)*s(2535)
s(2577) =< s(2576)* (4/5)
s(2578) =< s(2576)* (2/3)
s(2579) =< s(2576)
s(2580) =< s(2578)
s(2581) =< s(2577)
s(2582) =< s(2577)
s(2580) =< s(2577)
s(2582) =< s(2572)
s(2580) =< s(2572)
s(2583) =< s(2572)
s(2584) =< s(2575)
s(2580) =< s(2584)* (1/3)+s(2578)
s(2581) =< s(2584)* (1/5)+s(2577)
s(2582) =< s(2584)* (1/5)+s(2577)
s(2580) =< s(2584)* (1/5)+s(2577)
s(2585) =< s(2574)
s(2586) =< s(2540)
s(2586) =< s(2539)
s(2586) =< s(2545)
s(2587) =< s(2549)* (6/5)
s(2588) =< s(2545)
s(2589) =< s(2549)
s(2590) =< s(2587)
s(2591) =< s(2587)
s(2589) =< s(2587)
s(2591) =< s(2537)
s(2589) =< s(2537)
s(2589) =< s(2552)* (1/3)+s(2549)
s(2590) =< s(2552)* (1/5)+s(2587)
s(2591) =< s(2552)* (1/5)+s(2587)
s(2589) =< s(2552)* (1/5)+s(2587)
s(2592) =< s(2548)
s(2593) =< s(2547)
s(2594) =< s(2547)
s(2592) =< s(2547)
s(2594) =< aux(214)
s(2592) =< aux(214)
s(2592) =< s(2552)* (1/3)+s(2548)
s(2593) =< s(2552)* (1/5)+s(2547)
s(2594) =< s(2552)* (1/5)+s(2547)
s(2592) =< s(2552)* (1/5)+s(2547)
s(2595) =< s(2540)
s(2596) =< s(2546)
s(2597) =< s(2546)
s(2595) =< s(2546)
s(2597) =< s(2540)
s(2598) =< s(2540)
s(2598) =< s(2545)
s(2595) =< s(2558)* (1/3)+s(2540)
s(2596) =< s(2558)* (1/5)+s(2546)
s(2597) =< s(2558)* (1/5)+s(2546)
s(2595) =< s(2558)* (1/5)+s(2546)
s(2599) =< s(2540)
s(2600) =< s(2540)
s(2599) =< aux(214)
s(2600) =< aux(214)
s(2601) =< s(2600)*aux(214)
s(2602) =< s(2599)*2
s(2603) =< s(2600)*s(2535)
s(2604) =< s(2603)* (4/5)
s(2605) =< s(2603)* (2/3)
s(2606) =< s(2603)
s(2607) =< s(2605)
s(2608) =< s(2604)
s(2609) =< s(2604)
s(2607) =< s(2604)
s(2609) =< s(2599)
s(2607) =< s(2599)
s(2610) =< s(2599)
s(2611) =< s(2602)
s(2607) =< s(2611)* (1/3)+s(2605)
s(2608) =< s(2611)* (1/5)+s(2604)
s(2609) =< s(2611)* (1/5)+s(2604)
s(2607) =< s(2611)* (1/5)+s(2604)
s(2612) =< s(2601)
s(2613) =< s(2532)* (1/2)+1/2
s(2614) =< s(2573)*s(2532)
s(2615) =< s(2573)*s(2613)
s(2616) =< s(2615)* (4/5)
s(2617) =< s(2615)* (2/3)
s(2618) =< s(2615)
s(2619) =< s(2617)
s(2620) =< s(2616)
s(2621) =< s(2616)
s(2619) =< s(2616)
s(2621) =< s(2572)
s(2619) =< s(2572)
s(2619) =< s(2584)* (1/3)+s(2617)
s(2620) =< s(2584)* (1/5)+s(2616)
s(2621) =< s(2584)* (1/5)+s(2616)
s(2619) =< s(2584)* (1/5)+s(2616)
s(2622) =< s(2614)
s(2623) =< s(2544)
s(2624) =< s(2538)
s(2625) =< s(2543)
s(2626) =< s(2543)
s(2624) =< s(2543)
s(2626) =< s(2540)
s(2624) =< s(2540)
s(2624) =< s(2558)* (1/3)+s(2538)
s(2625) =< s(2558)* (1/5)+s(2543)
s(2626) =< s(2558)* (1/5)+s(2543)
s(2624) =< s(2558)* (1/5)+s(2543)
s(2628) =< aux(214)
s(2629) =< aux(214)
s(2628) =< aux(216)
s(2629) =< aux(216)
s(2630) =< s(2628)* (1/2)
s(2631) =< s(2628)*2
s(2632) =< s(2629)*aux(214)
s(2633) =< s(2629)*s(2531)
s(2634) =< s(2629)*s(2532)
s(2636) =< s(2629)*s(2534)
s(2637) =< s(2632)* (6/5)
s(2638) =< s(2629)*s(2535)
s(2639) =< s(2633)* (1/2)
s(2640) =< s(2634)* (6/5)
s(2641) =< s(2633)* (2/5)
s(2642) =< s(2633)* (1/3)
s(2643) =< s(2636)* (1/3)
s(2644) =< s(2633)*2
s(2645) =< s(2634)
s(2646) =< s(2628)
s(2647) =< s(2631)
s(2648) =< s(2634)
s(2648) =< s(2633)
s(2649) =< s(2633)
s(2650) =< s(2633)
s(2650) =< s(2631)
s(2649) =< s(2628)
s(2651) =< s(2631)* (1/2)
s(2652) =< s(2636)* (6/5)
s(2653) =< s(2633)
s(2654) =< s(2636)
s(2655) =< s(2652)
s(2656) =< s(2652)
s(2654) =< s(2652)
s(2656) =< s(2631)
s(2654) =< s(2631)
s(2657) =< s(2631)
s(2657) =< s(2651)
s(2654) =< s(2647)* (1/3)+s(2636)
s(2655) =< s(2647)* (1/5)+s(2652)
s(2656) =< s(2647)* (1/5)+s(2652)
s(2654) =< s(2647)* (1/5)+s(2652)
s(2658) =< s(2628)
s(2658) =< s(2631)
s(2659) =< s(2628)* (6/5)
s(2660) =< s(2630)
s(2661) =< s(2628)
s(2662) =< s(2659)
s(2663) =< s(2659)
s(2661) =< s(2659)
s(2663) =< s(2631)
s(2661) =< s(2631)
s(2661) =< s(2647)* (1/3)+s(2628)
s(2662) =< s(2647)* (1/5)+s(2659)
s(2663) =< s(2647)* (1/5)+s(2659)
s(2661) =< s(2647)* (1/5)+s(2659)
s(2664) =< s(2633)
s(2665) =< s(2644)
s(2666) =< s(2644)
s(2664) =< s(2644)
s(2666) =< s(2628)
s(2664) =< s(2628)
s(2664) =< s(2647)* (1/3)+s(2633)
s(2665) =< s(2647)* (1/5)+s(2644)
s(2666) =< s(2647)* (1/5)+s(2644)
s(2664) =< s(2647)* (1/5)+s(2644)
s(2667) =< s(2634)
s(2668) =< s(2634)
s(2667) =< s(2644)
s(2668) =< s(2644)
s(2669) =< s(2668)*aux(214)
s(2670) =< s(2667)*2
s(2671) =< s(2668)*s(2535)
s(2672) =< s(2671)* (4/5)
s(2673) =< s(2671)* (2/3)
s(2674) =< s(2671)
s(2675) =< s(2673)
s(2676) =< s(2672)
s(2677) =< s(2672)
s(2675) =< s(2672)
s(2677) =< s(2667)
s(2675) =< s(2667)
s(2678) =< s(2667)
s(2679) =< s(2670)
s(2675) =< s(2679)* (1/3)+s(2673)
s(2676) =< s(2679)* (1/5)+s(2672)
s(2677) =< s(2679)* (1/5)+s(2672)
s(2675) =< s(2679)* (1/5)+s(2672)
s(2680) =< s(2669)
s(2681) =< s(2634)
s(2681) =< s(2633)
s(2681) =< s(2639)
s(2682) =< s(2643)* (6/5)
s(2683) =< s(2639)
s(2684) =< s(2643)
s(2685) =< s(2682)
s(2686) =< s(2682)
s(2684) =< s(2682)
s(2686) =< s(2631)
s(2684) =< s(2631)
s(2684) =< s(2647)* (1/3)+s(2643)
s(2685) =< s(2647)* (1/5)+s(2682)
s(2686) =< s(2647)* (1/5)+s(2682)
s(2684) =< s(2647)* (1/5)+s(2682)
s(2687) =< s(2642)
s(2688) =< s(2641)
s(2689) =< s(2641)
s(2687) =< s(2641)
s(2689) =< s(2628)
s(2687) =< s(2628)
s(2687) =< s(2647)* (1/3)+s(2642)
s(2688) =< s(2647)* (1/5)+s(2641)
s(2689) =< s(2647)* (1/5)+s(2641)
s(2687) =< s(2647)* (1/5)+s(2641)
s(2690) =< s(2634)
s(2691) =< s(2640)
s(2692) =< s(2640)
s(2690) =< s(2640)
s(2692) =< s(2634)
s(2693) =< s(2634)
s(2693) =< s(2639)
s(2690) =< s(2653)* (1/3)+s(2634)
s(2691) =< s(2653)* (1/5)+s(2640)
s(2692) =< s(2653)* (1/5)+s(2640)
s(2690) =< s(2653)* (1/5)+s(2640)
s(2694) =< s(2634)
s(2695) =< s(2634)
s(2694) =< s(2628)
s(2695) =< s(2628)
s(2696) =< s(2695)*aux(214)
s(2697) =< s(2694)*2
s(2698) =< s(2695)*s(2535)
s(2699) =< s(2698)* (4/5)
s(2700) =< s(2698)* (2/3)
s(2701) =< s(2698)
s(2702) =< s(2700)
s(2703) =< s(2699)
s(2704) =< s(2699)
s(2702) =< s(2699)
s(2704) =< s(2694)
s(2702) =< s(2694)
s(2705) =< s(2694)
s(2706) =< s(2697)
s(2702) =< s(2706)* (1/3)+s(2700)
s(2703) =< s(2706)* (1/5)+s(2699)
s(2704) =< s(2706)* (1/5)+s(2699)
s(2702) =< s(2706)* (1/5)+s(2699)
s(2707) =< s(2696)
s(2708) =< s(2668)*s(2532)
s(2709) =< s(2668)*s(2613)
s(2710) =< s(2709)* (4/5)
s(2711) =< s(2709)* (2/3)
s(2712) =< s(2709)
s(2713) =< s(2711)
s(2714) =< s(2710)
s(2715) =< s(2710)
s(2713) =< s(2710)
s(2715) =< s(2667)
s(2713) =< s(2667)
s(2713) =< s(2679)* (1/3)+s(2711)
s(2714) =< s(2679)* (1/5)+s(2710)
s(2715) =< s(2679)* (1/5)+s(2710)
s(2713) =< s(2679)* (1/5)+s(2710)
s(2716) =< s(2708)
s(2717) =< s(2638)
s(2718) =< s(2632)
s(2719) =< s(2637)
s(2720) =< s(2637)
s(2718) =< s(2637)
s(2720) =< s(2634)
s(2718) =< s(2634)
s(2718) =< s(2653)* (1/3)+s(2632)
s(2719) =< s(2653)* (1/5)+s(2637)
s(2720) =< s(2653)* (1/5)+s(2637)
s(2718) =< s(2653)* (1/5)+s(2637)
s(2474) =< aux(209)
s(2475) =< aux(209)
s(2474) =< aux(214)
s(2475) =< aux(214)
s(2474) =< aux(227)
s(2475) =< aux(227)
s(2477) =< s(2475)*aux(227)
s(2478) =< s(2474)*2
s(2479) =< s(2475)*s(2152)
s(2480) =< s(2479)* (4/5)
s(2481) =< s(2479)* (2/3)
s(2482) =< s(2479)
s(2483) =< s(2481)
s(2484) =< s(2480)
s(2485) =< s(2480)
s(2483) =< s(2480)
s(2485) =< s(2474)
s(2483) =< s(2474)
s(2486) =< s(2474)
s(2487) =< s(2478)
s(2483) =< s(2487)* (1/3)+s(2481)
s(2484) =< s(2487)* (1/5)+s(2480)
s(2485) =< s(2487)* (1/5)+s(2480)
s(2483) =< s(2487)* (1/5)+s(2480)
s(2488) =< s(2477)
s(2730) =< aux(209)
s(2731) =< aux(209)
s(2730) =< aux(227)
s(2731) =< aux(227)
s(2733) =< s(2731)*aux(227)
s(2734) =< s(2730)*2
s(2735) =< s(2731)*s(2152)
s(2736) =< s(2735)* (4/5)
s(2737) =< s(2735)* (2/3)
s(2738) =< s(2735)
s(2739) =< s(2737)
s(2740) =< s(2736)
s(2741) =< s(2736)
s(2739) =< s(2736)
s(2741) =< s(2730)
s(2739) =< s(2730)
s(2742) =< s(2730)
s(2743) =< s(2734)
s(2739) =< s(2743)* (1/3)+s(2737)
s(2740) =< s(2743)* (1/5)+s(2736)
s(2741) =< s(2743)* (1/5)+s(2736)
s(2739) =< s(2743)* (1/5)+s(2736)
s(2744) =< s(2733)
s(2754) =< aux(209)
s(2755) =< aux(209)
s(2754) =< aux(213)
s(2755) =< aux(213)
s(2754) =< aux(227)
s(2755) =< aux(227)
s(2757) =< s(2755)*aux(227)
s(2758) =< s(2754)*2
s(2759) =< s(2755)*s(2152)
s(2760) =< s(2759)* (4/5)
s(2761) =< s(2759)* (2/3)
s(2762) =< s(2759)
s(2763) =< s(2761)
s(2764) =< s(2760)
s(2765) =< s(2760)
s(2763) =< s(2760)
s(2765) =< s(2754)
s(2763) =< s(2754)
s(2766) =< s(2754)
s(2767) =< s(2758)
s(2763) =< s(2767)* (1/3)+s(2761)
s(2764) =< s(2767)* (1/5)+s(2760)
s(2765) =< s(2767)* (1/5)+s(2760)
s(2763) =< s(2767)* (1/5)+s(2760)
s(2768) =< s(2757)
s(3545) =< aux(228)
s(3545) =< aux(220)
s(3303) =< aux(209)
s(3303) =< aux(220)
s(3252) =< aux(209)* (1/2)+1/2
s(3518) =< s(2475)*aux(209)
s(3520) =< s(2475)*s(3252)
s(3521) =< s(3520)* (4/5)
s(3522) =< s(3520)* (2/3)
s(3523) =< s(3520)
s(3524) =< s(3522)
s(3525) =< s(3521)
s(3526) =< s(3521)
s(3524) =< s(3521)
s(3526) =< s(2474)
s(3524) =< s(2474)
s(3524) =< s(2487)* (1/3)+s(3522)
s(3525) =< s(2487)* (1/5)+s(3521)
s(3526) =< s(2487)* (1/5)+s(3521)
s(3524) =< s(2487)* (1/5)+s(3521)
s(3529) =< s(3518)
s(3771) =< aux(227)
s(3772) =< aux(227)
s(3771) =< aux(208)
s(3772) =< aux(208)
s(3771) =< aux(209)
s(3772) =< aux(209)
s(3774) =< s(3772)*aux(209)
s(3775) =< s(3771)*2
s(3776) =< s(3772)*s(3252)
s(3777) =< s(3776)* (4/5)
s(3778) =< s(3776)* (2/3)
s(3779) =< s(3776)
s(3780) =< s(3778)
s(3781) =< s(3777)
s(3782) =< s(3777)
s(3780) =< s(3777)
s(3782) =< s(3771)
s(3780) =< s(3771)
s(3783) =< s(3771)
s(3784) =< s(3775)
s(3780) =< s(3784)* (1/3)+s(3778)
s(3781) =< s(3784)* (1/5)+s(3777)
s(3782) =< s(3784)* (1/5)+s(3777)
s(3780) =< s(3784)* (1/5)+s(3777)
s(3785) =< s(3774)
s(4545) =< aux(227)
s(4546) =< aux(227)
s(4545) =< aux(216)
s(4546) =< aux(216)
s(4545) =< aux(209)
s(4546) =< aux(209)
s(4548) =< s(4546)*aux(209)
s(4549) =< s(4545)*2
s(4550) =< s(4546)*s(3252)
s(4551) =< s(4550)* (4/5)
s(4552) =< s(4550)* (2/3)
s(4553) =< s(4550)
s(4554) =< s(4552)
s(4555) =< s(4551)
s(4556) =< s(4551)
s(4554) =< s(4551)
s(4556) =< s(4545)
s(4554) =< s(4545)
s(4557) =< s(4545)
s(4558) =< s(4549)
s(4554) =< s(4558)* (1/3)+s(4552)
s(4555) =< s(4558)* (1/5)+s(4551)
s(4556) =< s(4558)* (1/5)+s(4551)
s(4554) =< s(4558)* (1/5)+s(4551)
s(4559) =< s(4548)
s(4680) =< aux(227)
s(4681) =< aux(227)
s(4681) =< aux(206)
s(4680) =< aux(205)
s(2208) =< aux(229)* (6/5)
s(4685) =< aux(229)
s(4686) =< s(2208)
s(4687) =< s(2208)
s(4685) =< s(2208)
s(4687) =< aux(206)
s(4685) =< aux(206)
s(4685) =< s(2129)* (1/3)+aux(229)
s(4686) =< s(2129)* (1/5)+s(2208)
s(4687) =< s(2129)* (1/5)+s(2208)
s(4685) =< s(2129)* (1/5)+s(2208)
s(4695) =< aux(227)
s(4696) =< aux(231)
s(4697) =< aux(231)
s(4695) =< aux(231)
s(4697) =< aux(205)
s(4695) =< aux(205)
s(4695) =< s(2129)* (1/3)+aux(227)
s(4696) =< s(2129)* (1/5)+aux(231)
s(4697) =< s(2129)* (1/5)+aux(231)
s(4695) =< s(2129)* (1/5)+aux(231)
s(4698) =< aux(209)
s(4699) =< aux(209)
s(4698) =< aux(227)
s(4699) =< aux(227)
s(4698) =< aux(231)
s(4699) =< aux(231)
s(4701) =< s(4699)*aux(227)
s(4702) =< s(4698)*2
s(4703) =< s(4699)*s(2152)
s(4704) =< s(4703)* (4/5)
s(4705) =< s(4703)* (2/3)
s(4706) =< s(4703)
s(4707) =< s(4705)
s(4708) =< s(4704)
s(4709) =< s(4704)
s(4707) =< s(4704)
s(4709) =< s(4698)
s(4707) =< s(4698)
s(4710) =< s(4698)
s(4711) =< s(4702)
s(4707) =< s(4711)* (1/3)+s(4705)
s(4708) =< s(4711)* (1/5)+s(4704)
s(4709) =< s(4711)* (1/5)+s(4704)
s(4707) =< s(4711)* (1/5)+s(4704)
s(4712) =< s(4701)
s(4713) =< aux(227)
s(4713) =< s(4667)
s(2193) =< aux(237)* (6/5)
s(4715) =< s(4667)
s(4716) =< aux(237)
s(4717) =< s(2193)
s(4718) =< s(2193)
s(4716) =< s(2193)
s(4718) =< aux(206)
s(4716) =< aux(206)
s(4716) =< s(2129)* (1/3)+aux(237)
s(4717) =< s(2129)* (1/5)+s(2193)
s(4718) =< s(2129)* (1/5)+s(2193)
s(4716) =< s(2129)* (1/5)+s(2193)
s(4719) =< aux(234)
s(4720) =< aux(238)
s(4721) =< aux(238)
s(4719) =< aux(238)
s(4721) =< aux(205)
s(4719) =< aux(205)
s(4719) =< s(2129)* (1/3)+aux(234)
s(4720) =< s(2129)* (1/5)+aux(238)
s(4721) =< s(2129)* (1/5)+aux(238)
s(4719) =< s(2129)* (1/5)+aux(238)
s(2189) =< aux(228)
s(2189) =< aux(207)
s(2192) =< aux(205)* (1/2)
s(2195) =< aux(237)
s(2196) =< s(2193)
s(2197) =< s(2193)
s(2195) =< s(2193)
s(2197) =< aux(205)
s(2195) =< aux(205)
s(2198) =< aux(205)
s(2198) =< s(2192)
s(2195) =< s(2128)* (1/3)+aux(237)
s(2196) =< s(2128)* (1/5)+s(2193)
s(2197) =< s(2128)* (1/5)+s(2193)
s(2195) =< s(2128)* (1/5)+s(2193)
s(2201) =< aux(238)
s(2201) =< s(2128)* (1/5)+aux(238)
s(2207) =< aux(228)* (1/2)
s(2209) =< aux(229)
s(2210) =< s(2208)
s(2211) =< s(2208)
s(2209) =< s(2208)
s(2211) =< aux(228)
s(2209) =< aux(228)
s(2212) =< aux(228)
s(2212) =< s(2207)
s(2209) =< s(2136)* (1/3)+aux(229)
s(2210) =< s(2136)* (1/5)+s(2208)
s(2211) =< s(2136)* (1/5)+s(2208)
s(2209) =< s(2136)* (1/5)+s(2208)
s(2213) =< aux(227)
s(2214) =< aux(231)
s(2215) =< aux(231)
s(2213) =< aux(231)
s(2215) =< aux(227)
s(2213) =< s(2136)* (1/3)+aux(227)
s(2214) =< s(2136)* (1/5)+aux(231)
s(2215) =< s(2136)* (1/5)+aux(231)
s(2213) =< s(2136)* (1/5)+aux(231)
s(2216) =< aux(227)+1
s(2217) =< aux(227)
s(2218) =< aux(234)
s(2219) =< aux(227)+3
s(2221) =< aux(227)* (1/2)
s(2222) =< aux(227)*2
s(2223) =< s(2112)*aux(234)
s(2224) =< s(2112)*s(2216)
s(2225) =< s(2112)*s(2217)
s(2226) =< s(2112)*s(2218)
s(2227) =< s(2112)*s(2219)
s(2228) =< s(2223)* (6/5)
s(2229) =< s(2112)*s(2152)
s(2230) =< s(2224)* (1/2)
s(2231) =< s(2226)* (6/5)
s(2232) =< s(2224)* (2/5)
s(2233) =< s(2224)* (1/3)
s(2234) =< s(2227)* (1/3)
s(2235) =< s(2224)*2
s(2236) =< s(2225)
s(2237) =< s(2222)
s(2238) =< s(2225)
s(2238) =< s(2224)
s(2239) =< s(2224)
s(2240) =< s(2224)
s(2240) =< s(2222)
s(2239) =< aux(227)
s(2241) =< s(2222)* (1/2)
s(2242) =< s(2227)* (6/5)
s(2243) =< s(2224)
s(2244) =< s(2227)
s(2245) =< s(2242)
s(2246) =< s(2242)
s(2244) =< s(2242)
s(2246) =< s(2222)
s(2244) =< s(2222)
s(2247) =< s(2222)
s(2247) =< s(2241)
s(2244) =< s(2237)* (1/3)+s(2227)
s(2245) =< s(2237)* (1/5)+s(2242)
s(2246) =< s(2237)* (1/5)+s(2242)
s(2244) =< s(2237)* (1/5)+s(2242)
s(2248) =< aux(227)
s(2248) =< s(2222)
s(2249) =< aux(227)* (6/5)
s(2250) =< s(2221)
s(2251) =< aux(227)
s(2252) =< s(2249)
s(2253) =< s(2249)
s(2251) =< s(2249)
s(2253) =< s(2222)
s(2251) =< s(2222)
s(2251) =< s(2237)* (1/3)+aux(227)
s(2252) =< s(2237)* (1/5)+s(2249)
s(2253) =< s(2237)* (1/5)+s(2249)
s(2251) =< s(2237)* (1/5)+s(2249)
s(2254) =< s(2224)
s(2255) =< s(2235)
s(2256) =< s(2235)
s(2254) =< s(2235)
s(2256) =< aux(227)
s(2254) =< aux(227)
s(2254) =< s(2237)* (1/3)+s(2224)
s(2255) =< s(2237)* (1/5)+s(2235)
s(2256) =< s(2237)* (1/5)+s(2235)
s(2254) =< s(2237)* (1/5)+s(2235)
s(2257) =< s(2225)
s(2258) =< s(2225)
s(2257) =< s(2235)
s(2258) =< s(2235)
s(2259) =< s(2258)*aux(227)
s(2260) =< s(2257)*2
s(2261) =< s(2258)*s(2152)
s(2262) =< s(2261)* (4/5)
s(2263) =< s(2261)* (2/3)
s(2264) =< s(2261)
s(2265) =< s(2263)
s(2266) =< s(2262)
s(2267) =< s(2262)
s(2265) =< s(2262)
s(2267) =< s(2257)
s(2265) =< s(2257)
s(2268) =< s(2257)
s(2269) =< s(2260)
s(2265) =< s(2269)* (1/3)+s(2263)
s(2266) =< s(2269)* (1/5)+s(2262)
s(2267) =< s(2269)* (1/5)+s(2262)
s(2265) =< s(2269)* (1/5)+s(2262)
s(2270) =< s(2259)
s(2271) =< s(2225)
s(2271) =< s(2224)
s(2271) =< s(2230)
s(2272) =< s(2234)* (6/5)
s(2273) =< s(2230)
s(2274) =< s(2234)
s(2275) =< s(2272)
s(2276) =< s(2272)
s(2274) =< s(2272)
s(2276) =< s(2222)
s(2274) =< s(2222)
s(2274) =< s(2237)* (1/3)+s(2234)
s(2275) =< s(2237)* (1/5)+s(2272)
s(2276) =< s(2237)* (1/5)+s(2272)
s(2274) =< s(2237)* (1/5)+s(2272)
s(2277) =< s(2233)
s(2278) =< s(2232)
s(2279) =< s(2232)
s(2277) =< s(2232)
s(2279) =< aux(227)
s(2277) =< aux(227)
s(2277) =< s(2237)* (1/3)+s(2233)
s(2278) =< s(2237)* (1/5)+s(2232)
s(2279) =< s(2237)* (1/5)+s(2232)
s(2277) =< s(2237)* (1/5)+s(2232)
s(2280) =< s(2226)
s(2281) =< s(2231)
s(2282) =< s(2231)
s(2280) =< s(2231)
s(2282) =< s(2225)
s(2280) =< s(2225)
s(2283) =< s(2225)
s(2283) =< s(2230)
s(2280) =< s(2243)* (1/3)+s(2226)
s(2281) =< s(2243)* (1/5)+s(2231)
s(2282) =< s(2243)* (1/5)+s(2231)
s(2280) =< s(2243)* (1/5)+s(2231)
s(2284) =< s(2225)
s(2285) =< s(2225)
s(2284) =< aux(227)
s(2285) =< aux(227)
s(2286) =< s(2285)*aux(227)
s(2287) =< s(2284)*2
s(2288) =< s(2285)*s(2152)
s(2289) =< s(2288)* (4/5)
s(2290) =< s(2288)* (2/3)
s(2291) =< s(2288)
s(2292) =< s(2290)
s(2293) =< s(2289)
s(2294) =< s(2289)
s(2292) =< s(2289)
s(2294) =< s(2284)
s(2292) =< s(2284)
s(2295) =< s(2284)
s(2296) =< s(2287)
s(2292) =< s(2296)* (1/3)+s(2290)
s(2293) =< s(2296)* (1/5)+s(2289)
s(2294) =< s(2296)* (1/5)+s(2289)
s(2292) =< s(2296)* (1/5)+s(2289)
s(2297) =< s(2286)
s(2298) =< s(2217)* (1/2)+1/2
s(2299) =< s(2258)*s(2217)
s(2300) =< s(2258)*s(2298)
s(2301) =< s(2300)* (4/5)
s(2302) =< s(2300)* (2/3)
s(2303) =< s(2300)
s(2304) =< s(2302)
s(2305) =< s(2301)
s(2306) =< s(2301)
s(2304) =< s(2301)
s(2306) =< s(2257)
s(2304) =< s(2257)
s(2304) =< s(2269)* (1/3)+s(2302)
s(2305) =< s(2269)* (1/5)+s(2301)
s(2306) =< s(2269)* (1/5)+s(2301)
s(2304) =< s(2269)* (1/5)+s(2301)
s(2307) =< s(2299)
s(2308) =< s(2229)
s(2309) =< s(2223)
s(2310) =< s(2228)
s(2311) =< s(2228)
s(2309) =< s(2228)
s(2311) =< s(2225)
s(2309) =< s(2225)
s(2309) =< s(2243)* (1/3)+s(2223)
s(2310) =< s(2243)* (1/5)+s(2228)
s(2311) =< s(2243)* (1/5)+s(2228)
s(2309) =< s(2243)* (1/5)+s(2228)
s(2312) =< aux(229)
s(2313) =< aux(227)
s(2314) =< aux(227)
s(2313) =< aux(229)
s(2314) =< aux(229)
s(2315) =< s(2313)* (1/2)
s(2316) =< s(2313)*2
s(2317) =< s(2314)*aux(234)
s(2318) =< s(2314)*s(2216)
s(2319) =< s(2314)*s(2217)
s(2320) =< s(2314)*s(2218)
s(2321) =< s(2314)*s(2219)
s(2322) =< s(2317)* (6/5)
s(2323) =< s(2314)*s(2152)
s(2324) =< s(2318)* (1/2)
s(2325) =< s(2320)* (6/5)
s(2326) =< s(2318)* (2/5)
s(2327) =< s(2318)* (1/3)
s(2328) =< s(2321)* (1/3)
s(2329) =< s(2318)*2
s(2330) =< s(2319)
s(2331) =< s(2313)
s(2332) =< s(2316)
s(2333) =< s(2319)
s(2333) =< s(2318)
s(2334) =< s(2318)
s(2335) =< s(2318)
s(2335) =< s(2316)
s(2334) =< s(2313)
s(2336) =< s(2316)* (1/2)
s(2337) =< s(2321)* (6/5)
s(2338) =< s(2318)
s(2339) =< s(2321)
s(2340) =< s(2337)
s(2341) =< s(2337)
s(2339) =< s(2337)
s(2341) =< s(2316)
s(2339) =< s(2316)
s(2342) =< s(2316)
s(2342) =< s(2336)
s(2339) =< s(2332)* (1/3)+s(2321)
s(2340) =< s(2332)* (1/5)+s(2337)
s(2341) =< s(2332)* (1/5)+s(2337)
s(2339) =< s(2332)* (1/5)+s(2337)
s(2343) =< s(2313)
s(2343) =< s(2316)
s(2344) =< s(2313)* (6/5)
s(2345) =< s(2315)
s(2346) =< s(2313)
s(2347) =< s(2344)
s(2348) =< s(2344)
s(2346) =< s(2344)
s(2348) =< s(2316)
s(2346) =< s(2316)
s(2346) =< s(2332)* (1/3)+s(2313)
s(2347) =< s(2332)* (1/5)+s(2344)
s(2348) =< s(2332)* (1/5)+s(2344)
s(2346) =< s(2332)* (1/5)+s(2344)
s(2349) =< s(2318)
s(2350) =< s(2329)
s(2351) =< s(2329)
s(2349) =< s(2329)
s(2351) =< s(2313)
s(2349) =< s(2313)
s(2349) =< s(2332)* (1/3)+s(2318)
s(2350) =< s(2332)* (1/5)+s(2329)
s(2351) =< s(2332)* (1/5)+s(2329)
s(2349) =< s(2332)* (1/5)+s(2329)
s(2352) =< s(2319)
s(2353) =< s(2319)
s(2352) =< s(2329)
s(2353) =< s(2329)
s(2354) =< s(2353)*aux(227)
s(2355) =< s(2352)*2
s(2356) =< s(2353)*s(2152)
s(2357) =< s(2356)* (4/5)
s(2358) =< s(2356)* (2/3)
s(2359) =< s(2356)
s(2360) =< s(2358)
s(2361) =< s(2357)
s(2362) =< s(2357)
s(2360) =< s(2357)
s(2362) =< s(2352)
s(2360) =< s(2352)
s(2363) =< s(2352)
s(2364) =< s(2355)
s(2360) =< s(2364)* (1/3)+s(2358)
s(2361) =< s(2364)* (1/5)+s(2357)
s(2362) =< s(2364)* (1/5)+s(2357)
s(2360) =< s(2364)* (1/5)+s(2357)
s(2365) =< s(2354)
s(2366) =< s(2319)
s(2366) =< s(2318)
s(2366) =< s(2324)
s(2367) =< s(2328)* (6/5)
s(2368) =< s(2324)
s(2369) =< s(2328)
s(2370) =< s(2367)
s(2371) =< s(2367)
s(2369) =< s(2367)
s(2371) =< s(2316)
s(2369) =< s(2316)
s(2369) =< s(2332)* (1/3)+s(2328)
s(2370) =< s(2332)* (1/5)+s(2367)
s(2371) =< s(2332)* (1/5)+s(2367)
s(2369) =< s(2332)* (1/5)+s(2367)
s(2372) =< s(2327)
s(2373) =< s(2326)
s(2374) =< s(2326)
s(2372) =< s(2326)
s(2374) =< s(2313)
s(2372) =< s(2313)
s(2372) =< s(2332)* (1/3)+s(2327)
s(2373) =< s(2332)* (1/5)+s(2326)
s(2374) =< s(2332)* (1/5)+s(2326)
s(2372) =< s(2332)* (1/5)+s(2326)
s(2375) =< s(2320)
s(2376) =< s(2325)
s(2377) =< s(2325)
s(2375) =< s(2325)
s(2377) =< s(2319)
s(2375) =< s(2319)
s(2378) =< s(2319)
s(2378) =< s(2324)
s(2375) =< s(2338)* (1/3)+s(2320)
s(2376) =< s(2338)* (1/5)+s(2325)
s(2377) =< s(2338)* (1/5)+s(2325)
s(2375) =< s(2338)* (1/5)+s(2325)
s(2379) =< s(2319)
s(2380) =< s(2319)
s(2379) =< s(2313)
s(2380) =< s(2313)
s(2381) =< s(2380)*aux(227)
s(2382) =< s(2379)*2
s(2383) =< s(2380)*s(2152)
s(2384) =< s(2383)* (4/5)
s(2385) =< s(2383)* (2/3)
s(2386) =< s(2383)
s(2387) =< s(2385)
s(2388) =< s(2384)
s(2389) =< s(2384)
s(2387) =< s(2384)
s(2389) =< s(2379)
s(2387) =< s(2379)
s(2390) =< s(2379)
s(2391) =< s(2382)
s(2387) =< s(2391)* (1/3)+s(2385)
s(2388) =< s(2391)* (1/5)+s(2384)
s(2389) =< s(2391)* (1/5)+s(2384)
s(2387) =< s(2391)* (1/5)+s(2384)
s(2392) =< s(2381)
s(2393) =< s(2353)*s(2217)
s(2394) =< s(2353)*s(2298)
s(2395) =< s(2394)* (4/5)
s(2396) =< s(2394)* (2/3)
s(2397) =< s(2394)
s(2398) =< s(2396)
s(2399) =< s(2395)
s(2400) =< s(2395)
s(2398) =< s(2395)
s(2400) =< s(2352)
s(2398) =< s(2352)
s(2398) =< s(2364)* (1/3)+s(2396)
s(2399) =< s(2364)* (1/5)+s(2395)
s(2400) =< s(2364)* (1/5)+s(2395)
s(2398) =< s(2364)* (1/5)+s(2395)
s(2401) =< s(2393)
s(2402) =< s(2323)
s(2403) =< s(2317)
s(2404) =< s(2322)
s(2405) =< s(2322)
s(2403) =< s(2322)
s(2405) =< s(2319)
s(2403) =< s(2319)
s(2403) =< s(2338)* (1/3)+s(2317)
s(2404) =< s(2338)* (1/5)+s(2322)
s(2405) =< s(2338)* (1/5)+s(2322)
s(2403) =< s(2338)* (1/5)+s(2322)
s(3289) =< aux(205)
s(3232) =< aux(205)
s(3232) =< aux(210)
s(3289) =< aux(220)
s(3293) =< aux(224)* (6/5)
s(3295) =< aux(224)
s(3296) =< s(3293)
s(3297) =< s(3293)
s(3295) =< s(3293)
s(3297) =< aux(210)
s(3295) =< aux(210)
s(3295) =< s(2506)* (1/3)+aux(224)
s(3296) =< s(2506)* (1/5)+s(3293)
s(3297) =< s(2506)* (1/5)+s(3293)
s(3295) =< s(2506)* (1/5)+s(3293)
s(3300) =< aux(221)
s(3301) =< aux(225)
s(3302) =< aux(225)
s(3300) =< aux(225)
s(3302) =< aux(209)
s(3300) =< aux(209)
s(3300) =< s(2506)* (1/3)+aux(221)
s(3301) =< s(2506)* (1/5)+aux(225)
s(3302) =< s(2506)* (1/5)+aux(225)
s(3300) =< s(2506)* (1/5)+aux(225)
s(3308) =< aux(211)* (6/5)
s(3309) =< aux(211)
s(3310) =< s(3308)
s(3311) =< s(3308)
s(3309) =< s(3308)
s(3311) =< aux(210)
s(3309) =< aux(210)
s(3309) =< s(2506)* (1/3)+aux(211)
s(3310) =< s(2506)* (1/5)+s(3308)
s(3311) =< s(2506)* (1/5)+s(3308)
s(3309) =< s(2506)* (1/5)+s(3308)
s(3313) =< aux(209)
s(3314) =< aux(217)
s(3315) =< aux(217)
s(3313) =< aux(217)
s(3315) =< aux(209)
s(3313) =< s(2506)* (1/3)+aux(209)
s(3314) =< s(2506)* (1/5)+aux(217)
s(3315) =< s(2506)* (1/5)+aux(217)
s(3313) =< s(2506)* (1/5)+aux(217)
s(3316) =< aux(209)+1
s(3317) =< aux(209)
s(3318) =< aux(221)
s(3319) =< aux(209)+3
s(3321) =< aux(209)* (1/2)
s(3322) =< aux(209)*2
s(3323) =< s(2514)*aux(221)
s(3324) =< s(2514)*s(3316)
s(3325) =< s(2514)*s(3317)
s(3326) =< s(2514)*s(3318)
s(3327) =< s(2514)*s(3319)
s(3328) =< s(3323)* (6/5)
s(3329) =< s(2514)*s(3252)
s(3330) =< s(3324)* (1/2)
s(3331) =< s(3326)* (6/5)
s(3332) =< s(3324)* (2/5)
s(3333) =< s(3324)* (1/3)
s(3334) =< s(3327)* (1/3)
s(3335) =< s(3324)*2
s(3336) =< s(3325)
s(3337) =< s(3322)
s(3338) =< s(3325)
s(3338) =< s(3324)
s(3339) =< s(3324)
s(3340) =< s(3324)
s(3340) =< s(3322)
s(3339) =< aux(209)
s(3341) =< s(3322)* (1/2)
s(3342) =< s(3327)* (6/5)
s(3343) =< s(3324)
s(3344) =< s(3327)
s(3345) =< s(3342)
s(3346) =< s(3342)
s(3344) =< s(3342)
s(3346) =< s(3322)
s(3344) =< s(3322)
s(3347) =< s(3322)
s(3347) =< s(3341)
s(3344) =< s(3337)* (1/3)+s(3327)
s(3345) =< s(3337)* (1/5)+s(3342)
s(3346) =< s(3337)* (1/5)+s(3342)
s(3344) =< s(3337)* (1/5)+s(3342)
s(3348) =< aux(209)
s(3348) =< s(3322)
s(3349) =< aux(209)* (6/5)
s(3350) =< s(3321)
s(3351) =< aux(209)
s(3352) =< s(3349)
s(3353) =< s(3349)
s(3351) =< s(3349)
s(3353) =< s(3322)
s(3351) =< s(3322)
s(3351) =< s(3337)* (1/3)+aux(209)
s(3352) =< s(3337)* (1/5)+s(3349)
s(3353) =< s(3337)* (1/5)+s(3349)
s(3351) =< s(3337)* (1/5)+s(3349)
s(3354) =< s(3324)
s(3355) =< s(3335)
s(3356) =< s(3335)
s(3354) =< s(3335)
s(3356) =< aux(209)
s(3354) =< aux(209)
s(3354) =< s(3337)* (1/3)+s(3324)
s(3355) =< s(3337)* (1/5)+s(3335)
s(3356) =< s(3337)* (1/5)+s(3335)
s(3354) =< s(3337)* (1/5)+s(3335)
s(3357) =< s(3325)
s(3358) =< s(3325)
s(3357) =< s(3335)
s(3358) =< s(3335)
s(3359) =< s(3358)*aux(209)
s(3360) =< s(3357)*2
s(3361) =< s(3358)*s(3252)
s(3362) =< s(3361)* (4/5)
s(3363) =< s(3361)* (2/3)
s(3364) =< s(3361)
s(3365) =< s(3363)
s(3366) =< s(3362)
s(3367) =< s(3362)
s(3365) =< s(3362)
s(3367) =< s(3357)
s(3365) =< s(3357)
s(3368) =< s(3357)
s(3369) =< s(3360)
s(3365) =< s(3369)* (1/3)+s(3363)
s(3366) =< s(3369)* (1/5)+s(3362)
s(3367) =< s(3369)* (1/5)+s(3362)
s(3365) =< s(3369)* (1/5)+s(3362)
s(3370) =< s(3359)
s(3371) =< s(3325)
s(3371) =< s(3324)
s(3371) =< s(3330)
s(3372) =< s(3334)* (6/5)
s(3373) =< s(3330)
s(3374) =< s(3334)
s(3375) =< s(3372)
s(3376) =< s(3372)
s(3374) =< s(3372)
s(3376) =< s(3322)
s(3374) =< s(3322)
s(3374) =< s(3337)* (1/3)+s(3334)
s(3375) =< s(3337)* (1/5)+s(3372)
s(3376) =< s(3337)* (1/5)+s(3372)
s(3374) =< s(3337)* (1/5)+s(3372)
s(3377) =< s(3333)
s(3378) =< s(3332)
s(3379) =< s(3332)
s(3377) =< s(3332)
s(3379) =< aux(209)
s(3377) =< aux(209)
s(3377) =< s(3337)* (1/3)+s(3333)
s(3378) =< s(3337)* (1/5)+s(3332)
s(3379) =< s(3337)* (1/5)+s(3332)
s(3377) =< s(3337)* (1/5)+s(3332)
s(3380) =< s(3326)
s(3381) =< s(3331)
s(3382) =< s(3331)
s(3380) =< s(3331)
s(3382) =< s(3325)
s(3380) =< s(3325)
s(3383) =< s(3325)
s(3383) =< s(3330)
s(3380) =< s(3343)* (1/3)+s(3326)
s(3381) =< s(3343)* (1/5)+s(3331)
s(3382) =< s(3343)* (1/5)+s(3331)
s(3380) =< s(3343)* (1/5)+s(3331)
s(3384) =< s(3325)
s(3385) =< s(3325)
s(3384) =< aux(209)
s(3385) =< aux(209)
s(3386) =< s(3385)*aux(209)
s(3387) =< s(3384)*2
s(3388) =< s(3385)*s(3252)
s(3389) =< s(3388)* (4/5)
s(3390) =< s(3388)* (2/3)
s(3391) =< s(3388)
s(3392) =< s(3390)
s(3393) =< s(3389)
s(3394) =< s(3389)
s(3392) =< s(3389)
s(3394) =< s(3384)
s(3392) =< s(3384)
s(3395) =< s(3384)
s(3396) =< s(3387)
s(3392) =< s(3396)* (1/3)+s(3390)
s(3393) =< s(3396)* (1/5)+s(3389)
s(3394) =< s(3396)* (1/5)+s(3389)
s(3392) =< s(3396)* (1/5)+s(3389)
s(3397) =< s(3386)
s(3398) =< s(3317)* (1/2)+1/2
s(3399) =< s(3358)*s(3317)
s(3400) =< s(3358)*s(3398)
s(3401) =< s(3400)* (4/5)
s(3402) =< s(3400)* (2/3)
s(3403) =< s(3400)
s(3404) =< s(3402)
s(3405) =< s(3401)
s(3406) =< s(3401)
s(3404) =< s(3401)
s(3406) =< s(3357)
s(3404) =< s(3357)
s(3404) =< s(3369)* (1/3)+s(3402)
s(3405) =< s(3369)* (1/5)+s(3401)
s(3406) =< s(3369)* (1/5)+s(3401)
s(3404) =< s(3369)* (1/5)+s(3401)
s(3407) =< s(3399)
s(3408) =< s(3329)
s(3409) =< s(3323)
s(3410) =< s(3328)
s(3411) =< s(3328)
s(3409) =< s(3328)
s(3411) =< s(3325)
s(3409) =< s(3325)
s(3409) =< s(3343)* (1/3)+s(3323)
s(3410) =< s(3343)* (1/5)+s(3328)
s(3411) =< s(3343)* (1/5)+s(3328)
s(3409) =< s(3343)* (1/5)+s(3328)
s(3412) =< aux(211)
s(3413) =< aux(209)
s(3414) =< aux(209)
s(3413) =< aux(211)
s(3414) =< aux(211)
s(3415) =< s(3413)* (1/2)
s(3416) =< s(3413)*2
s(3417) =< s(3414)*aux(221)
s(3418) =< s(3414)*s(3316)
s(3419) =< s(3414)*s(3317)
s(3420) =< s(3414)*s(3318)
s(3421) =< s(3414)*s(3319)
s(3422) =< s(3417)* (6/5)
s(3423) =< s(3414)*s(3252)
s(3424) =< s(3418)* (1/2)
s(3425) =< s(3420)* (6/5)
s(3426) =< s(3418)* (2/5)
s(3427) =< s(3418)* (1/3)
s(3428) =< s(3421)* (1/3)
s(3429) =< s(3418)*2
s(3430) =< s(3419)
s(3431) =< s(3413)
s(3432) =< s(3416)
s(3433) =< s(3419)
s(3433) =< s(3418)
s(3434) =< s(3418)
s(3435) =< s(3418)
s(3435) =< s(3416)
s(3434) =< s(3413)
s(3436) =< s(3416)* (1/2)
s(3437) =< s(3421)* (6/5)
s(3438) =< s(3418)
s(3439) =< s(3421)
s(3440) =< s(3437)
s(3441) =< s(3437)
s(3439) =< s(3437)
s(3441) =< s(3416)
s(3439) =< s(3416)
s(3442) =< s(3416)
s(3442) =< s(3436)
s(3439) =< s(3432)* (1/3)+s(3421)
s(3440) =< s(3432)* (1/5)+s(3437)
s(3441) =< s(3432)* (1/5)+s(3437)
s(3439) =< s(3432)* (1/5)+s(3437)
s(3443) =< s(3413)
s(3443) =< s(3416)
s(3444) =< s(3413)* (6/5)
s(3445) =< s(3415)
s(3446) =< s(3413)
s(3447) =< s(3444)
s(3448) =< s(3444)
s(3446) =< s(3444)
s(3448) =< s(3416)
s(3446) =< s(3416)
s(3446) =< s(3432)* (1/3)+s(3413)
s(3447) =< s(3432)* (1/5)+s(3444)
s(3448) =< s(3432)* (1/5)+s(3444)
s(3446) =< s(3432)* (1/5)+s(3444)
s(3449) =< s(3418)
s(3450) =< s(3429)
s(3451) =< s(3429)
s(3449) =< s(3429)
s(3451) =< s(3413)
s(3449) =< s(3413)
s(3449) =< s(3432)* (1/3)+s(3418)
s(3450) =< s(3432)* (1/5)+s(3429)
s(3451) =< s(3432)* (1/5)+s(3429)
s(3449) =< s(3432)* (1/5)+s(3429)
s(3452) =< s(3419)
s(3453) =< s(3419)
s(3452) =< s(3429)
s(3453) =< s(3429)
s(3454) =< s(3453)*aux(209)
s(3455) =< s(3452)*2
s(3456) =< s(3453)*s(3252)
s(3457) =< s(3456)* (4/5)
s(3458) =< s(3456)* (2/3)
s(3459) =< s(3456)
s(3460) =< s(3458)
s(3461) =< s(3457)
s(3462) =< s(3457)
s(3460) =< s(3457)
s(3462) =< s(3452)
s(3460) =< s(3452)
s(3463) =< s(3452)
s(3464) =< s(3455)
s(3460) =< s(3464)* (1/3)+s(3458)
s(3461) =< s(3464)* (1/5)+s(3457)
s(3462) =< s(3464)* (1/5)+s(3457)
s(3460) =< s(3464)* (1/5)+s(3457)
s(3465) =< s(3454)
s(3466) =< s(3419)
s(3466) =< s(3418)
s(3466) =< s(3424)
s(3467) =< s(3428)* (6/5)
s(3468) =< s(3424)
s(3469) =< s(3428)
s(3470) =< s(3467)
s(3471) =< s(3467)
s(3469) =< s(3467)
s(3471) =< s(3416)
s(3469) =< s(3416)
s(3469) =< s(3432)* (1/3)+s(3428)
s(3470) =< s(3432)* (1/5)+s(3467)
s(3471) =< s(3432)* (1/5)+s(3467)
s(3469) =< s(3432)* (1/5)+s(3467)
s(3472) =< s(3427)
s(3473) =< s(3426)
s(3474) =< s(3426)
s(3472) =< s(3426)
s(3474) =< s(3413)
s(3472) =< s(3413)
s(3472) =< s(3432)* (1/3)+s(3427)
s(3473) =< s(3432)* (1/5)+s(3426)
s(3474) =< s(3432)* (1/5)+s(3426)
s(3472) =< s(3432)* (1/5)+s(3426)
s(3475) =< s(3420)
s(3476) =< s(3425)
s(3477) =< s(3425)
s(3475) =< s(3425)
s(3477) =< s(3419)
s(3475) =< s(3419)
s(3478) =< s(3419)
s(3478) =< s(3424)
s(3475) =< s(3438)* (1/3)+s(3420)
s(3476) =< s(3438)* (1/5)+s(3425)
s(3477) =< s(3438)* (1/5)+s(3425)
s(3475) =< s(3438)* (1/5)+s(3425)
s(3479) =< s(3419)
s(3480) =< s(3419)
s(3479) =< s(3413)
s(3480) =< s(3413)
s(3481) =< s(3480)*aux(209)
s(3482) =< s(3479)*2
s(3483) =< s(3480)*s(3252)
s(3484) =< s(3483)* (4/5)
s(3485) =< s(3483)* (2/3)
s(3486) =< s(3483)
s(3487) =< s(3485)
s(3488) =< s(3484)
s(3489) =< s(3484)
s(3487) =< s(3484)
s(3489) =< s(3479)
s(3487) =< s(3479)
s(3490) =< s(3479)
s(3491) =< s(3482)
s(3487) =< s(3491)* (1/3)+s(3485)
s(3488) =< s(3491)* (1/5)+s(3484)
s(3489) =< s(3491)* (1/5)+s(3484)
s(3487) =< s(3491)* (1/5)+s(3484)
s(3492) =< s(3481)
s(3493) =< s(3453)*s(3317)
s(3494) =< s(3453)*s(3398)
s(3495) =< s(3494)* (4/5)
s(3496) =< s(3494)* (2/3)
s(3497) =< s(3494)
s(3498) =< s(3496)
s(3499) =< s(3495)
s(3500) =< s(3495)
s(3498) =< s(3495)
s(3500) =< s(3452)
s(3498) =< s(3452)
s(3498) =< s(3464)* (1/3)+s(3496)
s(3499) =< s(3464)* (1/5)+s(3495)
s(3500) =< s(3464)* (1/5)+s(3495)
s(3498) =< s(3464)* (1/5)+s(3495)
s(3501) =< s(3493)
s(3502) =< s(3423)
s(3503) =< s(3417)
s(3504) =< s(3422)
s(3505) =< s(3422)
s(3503) =< s(3422)
s(3505) =< s(3419)
s(3503) =< s(3419)
s(3503) =< s(3438)* (1/3)+s(3417)
s(3504) =< s(3438)* (1/5)+s(3422)
s(3505) =< s(3438)* (1/5)+s(3422)
s(3503) =< s(3438)* (1/5)+s(3422)
s(3233) =< aux(210)
s(3233) =< aux(206)
s(3235) =< aux(212)* (6/5)
s(3237) =< aux(212)
s(3238) =< s(3235)
s(3239) =< s(3235)
s(3237) =< s(3235)
s(3239) =< aux(206)
s(3237) =< aux(206)
s(3237) =< s(2129)* (1/3)+aux(212)
s(3238) =< s(2129)* (1/5)+s(3235)
s(3239) =< s(2129)* (1/5)+s(3235)
s(3237) =< s(2129)* (1/5)+s(3235)
s(3247) =< aux(210)
s(3248) =< aux(218)
s(3249) =< aux(218)
s(3247) =< aux(218)
s(3249) =< aux(205)
s(3247) =< aux(205)
s(3247) =< s(2129)* (1/3)+aux(210)
s(3248) =< s(2129)* (1/5)+aux(218)
s(3249) =< s(2129)* (1/5)+aux(218)
s(3247) =< s(2129)* (1/5)+aux(218)
s(3250) =< aux(227)
s(3251) =< aux(227)
s(3250) =< aux(209)
s(3251) =< aux(209)
s(3250) =< aux(218)
s(3251) =< aux(218)
s(3253) =< s(3251)*aux(209)
s(3254) =< s(3250)*2
s(3255) =< s(3251)*s(3252)
s(3256) =< s(3255)* (4/5)
s(3257) =< s(3255)* (2/3)
s(3258) =< s(3255)
s(3259) =< s(3257)
s(3260) =< s(3256)
s(3261) =< s(3256)
s(3259) =< s(3256)
s(3261) =< s(3250)
s(3259) =< s(3250)
s(3262) =< s(3250)
s(3263) =< s(3254)
s(3259) =< s(3263)* (1/3)+s(3257)
s(3260) =< s(3263)* (1/5)+s(3256)
s(3261) =< s(3263)* (1/5)+s(3256)
s(3259) =< s(3263)* (1/5)+s(3256)
s(3264) =< s(3253)
s(3265) =< aux(209)
s(3265) =< aux(210)
s(3265) =< aux(220)
s(3266) =< aux(222)* (6/5)
s(3267) =< aux(220)
s(3268) =< aux(222)
s(3269) =< s(3266)
s(3270) =< s(3266)
s(3268) =< s(3266)
s(3270) =< aux(206)
s(3268) =< aux(206)
s(3268) =< s(2129)* (1/3)+aux(222)
s(3269) =< s(2129)* (1/5)+s(3266)
s(3270) =< s(2129)* (1/5)+s(3266)
s(3268) =< s(2129)* (1/5)+s(3266)
s(3271) =< aux(223)
s(3272) =< aux(226)
s(3273) =< aux(226)
s(3271) =< aux(226)
s(3273) =< aux(205)
s(3271) =< aux(205)
s(3271) =< s(2129)* (1/3)+aux(223)
s(3272) =< s(2129)* (1/5)+aux(226)
s(3273) =< s(2129)* (1/5)+aux(226)
s(3271) =< s(2129)* (1/5)+aux(226)
s(2998) =< aux(205)
s(2998) =< aux(207)
s(3002) =< s(2988)* (6/5)
s(3004) =< s(2988)
s(3005) =< s(3002)
s(3006) =< s(3002)
s(3004) =< s(3002)
s(3006) =< aux(205)
s(3004) =< aux(205)
s(3004) =< s(2128)* (1/3)+s(2988)
s(3005) =< s(2128)* (1/5)+s(3002)
s(3006) =< s(2128)* (1/5)+s(3002)
s(3004) =< s(2128)* (1/5)+s(3002)
s(3017) =< aux(206)* (6/5)
s(3018) =< aux(206)
s(3019) =< s(3017)
s(3020) =< s(3017)
s(3018) =< s(3017)
s(3020) =< aux(205)
s(3018) =< aux(205)
s(3018) =< s(2128)* (1/3)+aux(206)
s(3019) =< s(2128)* (1/5)+s(3017)
s(3020) =< s(2128)* (1/5)+s(3017)
s(3018) =< s(2128)* (1/5)+s(3017)
s(2944) =< s(2926)* (6/5)
s(2946) =< s(2926)
s(2947) =< s(2944)
s(2948) =< s(2944)
s(2946) =< s(2944)
s(2948) =< aux(206)
s(2946) =< aux(206)
s(2946) =< s(2129)* (1/3)+s(2926)
s(2947) =< s(2129)* (1/5)+s(2944)
s(2948) =< s(2129)* (1/5)+s(2944)
s(2946) =< s(2129)* (1/5)+s(2944)
s(2956) =< aux(205)
s(2957) =< aux(206)
s(2958) =< aux(206)
s(2956) =< aux(206)
s(2958) =< aux(205)
s(2956) =< s(2129)* (1/3)+aux(205)
s(2957) =< s(2129)* (1/5)+aux(206)
s(2958) =< s(2129)* (1/5)+aux(206)
s(2956) =< s(2129)* (1/5)+aux(206)
s(2980) =< s(2930)
s(2981) =< s(2931)
s(2982) =< s(2931)
s(2980) =< s(2931)
s(2982) =< aux(205)
s(2980) =< aux(205)
s(2980) =< s(2129)* (1/3)+s(2930)
s(2981) =< s(2129)* (1/5)+s(2931)
s(2982) =< s(2129)* (1/5)+s(2931)
s(2980) =< s(2129)* (1/5)+s(2931)
with precondition: [V=1,V1>=0,V35>=0]
* Chain [72]: 5*s(4745)+5*s(4746)+2
Such that:aux(240) =< V1
aux(241) =< V1+1
s(4745) =< aux(240)
s(4746) =< aux(241)
with precondition: [V=V1,V>=1]
* Chain [71]: 0
with precondition: [V=1,V1=2]
* Chain [70]: 1711/10
with precondition: [V=1,V35=0,V1>=1]
* Chain [69]: 0
with precondition: [V=2,V1=1]
* Chain [68]: 0
with precondition: [V=2,V1=2]
* Chain [67]: 39*s(5057)+66*s(5058)+247*s(5059)+7*s(5060)+5*s(5061)+4*s(5062)+30*s(5065)+2*s(5066)+2*s(5067)+2*s(5068)+8*s(5069)+4*s(5070)+4*s(5072)+4*s(5073)+4*s(5074)+4*s(5075)+2*s(5076)+2*s(5077)+2*s(5078)+6*s(5080)+2*s(5087)+2*s(5088)+2*s(5089)+2*s(5090)+2*s(5091)+6*s(5092)+24*s(5093)+4*s(5094)+14*s(5096)+2*s(5097)+2*s(5098)+2*s(5099)+2*s(5100)+2*s(5101)+2*s(5102)+1*s(5118)+1*s(5124)+1*s(5125)+1*s(5126)+1*s(5127)+4*s(5130)+1*s(5138)+1*s(5139)+1*s(5140)+1*s(5141)+4*s(5142)+4*s(5143)+4*s(5144)+384*s(5165)+180*s(5166)+6*s(5167)+12*s(5168)+12*s(5169)+48*s(5172)+6*s(5173)+6*s(5174)+6*s(5175)+24*s(5176)+12*s(5177)+12*s(5179)+12*s(5180)+12*s(5181)+12*s(5182)+6*s(5183)+6*s(5184)+6*s(5185)+18*s(5187)+3*s(5193)+3*s(5194)+3*s(5195)+3*s(5196)+6*s(5197)+18*s(5198)+36*s(5199)+6*s(5200)+18*s(5202)+6*s(5203)+6*s(5204)+6*s(5205)+6*s(5206)+6*s(5207)+6*s(5208)+9*s(5209)+9*s(5210)+9*s(5211)+12*s(5212)+18*s(5214)+6*s(5220)+6*s(5221)+6*s(5222)+6*s(5223)+6*s(5224)+18*s(5225)+72*s(5226)+3*s(5232)+3*s(5233)+3*s(5234)+3*s(5235)+36*s(5236)+6*s(5237)+3*s(5238)+3*s(5239)+3*s(5240)+1*s(5241)+10*s(5243)+128*s(5259)+16*s(5260)+60*s(5261)+2*s(5262)+4*s(5263)+4*s(5264)+16*s(5267)+2*s(5268)+2*s(5269)+2*s(5270)+8*s(5271)+4*s(5272)+4*s(5274)+4*s(5275)+4*s(5276)+4*s(5277)+2*s(5278)+2*s(5279)+2*s(5280)+6*s(5282)+1*s(5288)+1*s(5289)+1*s(5290)+1*s(5291)+2*s(5292)+6*s(5293)+12*s(5294)+2*s(5295)+6*s(5297)+2*s(5298)+2*s(5299)+2*s(5300)+2*s(5301)+2*s(5302)+2*s(5303)+3*s(5304)+3*s(5305)+3*s(5306)+4*s(5307)+6*s(5309)+2*s(5315)+2*s(5316)+2*s(5317)+2*s(5318)+2*s(5319)+6*s(5320)+24*s(5321)+1*s(5326)+1*s(5327)+1*s(5328)+1*s(5329)+12*s(5330)+2*s(5331)+1*s(5332)+1*s(5333)+1*s(5334)+3*s(5402)+1*s(5409)+1*s(5410)+1*s(5411)+1*s(5412)+1*s(5413)+3*s(5414)+12*s(5415)+2*s(5431)+17*s(5433)+1*s(5437)+1*s(5438)+1*s(5439)+1*s(5440)+3*s(5441)+4*s(5442)+4*s(5443)+4*s(5444)+4*s(5445)+84*s(5446)+5*s(5447)+24*s(5448)+1*s(5451)+1*s(5452)+1*s(5453)+1*s(5454)+4*s(5455)+4*s(5456)+4*s(5457)+384*s(5478)+180*s(5479)+6*s(5480)+12*s(5481)+12*s(5482)+48*s(5485)+6*s(5486)+6*s(5487)+6*s(5488)+24*s(5489)+12*s(5490)+12*s(5492)+12*s(5493)+12*s(5494)+12*s(5495)+6*s(5496)+6*s(5497)+6*s(5498)+18*s(5500)+3*s(5506)+3*s(5507)+3*s(5508)+3*s(5509)+6*s(5510)+18*s(5511)+36*s(5512)+6*s(5513)+18*s(5515)+6*s(5516)+6*s(5517)+6*s(5518)+6*s(5519)+6*s(5520)+6*s(5521)+9*s(5522)+9*s(5523)+9*s(5524)+12*s(5525)+18*s(5527)+6*s(5533)+6*s(5534)+6*s(5535)+6*s(5536)+6*s(5537)+18*s(5538)+72*s(5539)+3*s(5545)+3*s(5546)+3*s(5547)+3*s(5548)+36*s(5549)+6*s(5550)+3*s(5551)+3*s(5552)+3*s(5553)+2*s(5554)+20*s(5556)+256*s(5572)+32*s(5573)+120*s(5574)+4*s(5575)+8*s(5576)+8*s(5577)+32*s(5580)+4*s(5581)+4*s(5582)+4*s(5583)+16*s(5584)+8*s(5585)+8*s(5587)+8*s(5588)+8*s(5589)+8*s(5590)+4*s(5591)+4*s(5592)+4*s(5593)+12*s(5595)+2*s(5601)+2*s(5602)+2*s(5603)+2*s(5604)+4*s(5605)+12*s(5606)+24*s(5607)+4*s(5608)+12*s(5610)+4*s(5611)+4*s(5612)+4*s(5613)+4*s(5614)+4*s(5615)+4*s(5616)+6*s(5617)+6*s(5618)+6*s(5619)+8*s(5620)+12*s(5622)+4*s(5628)+4*s(5629)+4*s(5630)+4*s(5631)+4*s(5632)+12*s(5633)+48*s(5634)+2*s(5639)+2*s(5640)+2*s(5641)+2*s(5642)+24*s(5643)+4*s(5644)+2*s(5645)+2*s(5646)+2*s(5647)+3*s(5657)+1*s(5664)+1*s(5665)+1*s(5666)+1*s(5667)+1*s(5668)+3*s(5669)+12*s(5670)+6*s(5680)+2*s(5687)+2*s(5688)+2*s(5689)+2*s(5690)+2*s(5691)+6*s(5692)+24*s(5693)+3*s(5730)+1*s(5737)+1*s(5738)+1*s(5739)+1*s(5740)+1*s(5741)+3*s(5742)+12*s(5743)+5
Such that:aux(252) =< V1+1
s(5418) =< V1+V35+1
aux(255) =< 2*V1+2*V35
s(5114) =< V35+2
s(5106) =< 2*V35
s(5115) =< V35/3
s(5108) =< V35/3+2/3
s(5109) =< 2/5*V35
aux(262) =< 1
aux(263) =< 2
aux(264) =< 1/2
aux(265) =< V1
aux(266) =< V1-V35
aux(267) =< V1+V35
aux(268) =< V1+V35+2
aux(269) =< V35
aux(270) =< V35+1
aux(271) =< V35+3
aux(272) =< 2*V35+2
aux(273) =< V35/2+1/2
aux(274) =< V35/3+1
aux(275) =< V35/3+1/3
aux(276) =< 2/5*V35+2/5
s(5065) =< aux(270)
s(5057) =< aux(262)
s(5058) =< aux(263)
s(5059) =< aux(269)
s(5060) =< aux(269)
s(5060) =< aux(270)
s(5061) =< aux(270)
s(5062) =< aux(270)
s(5062) =< aux(263)
s(5061) =< aux(262)
s(5063) =< aux(263)* (1/2)
s(5064) =< aux(271)* (6/5)
s(5066) =< aux(271)
s(5067) =< s(5064)
s(5068) =< s(5064)
s(5066) =< s(5064)
s(5068) =< aux(263)
s(5066) =< aux(263)
s(5069) =< aux(263)
s(5069) =< s(5063)
s(5066) =< s(5058)* (1/3)+aux(271)
s(5067) =< s(5058)* (1/5)+s(5064)
s(5068) =< s(5058)* (1/5)+s(5064)
s(5066) =< s(5058)* (1/5)+s(5064)
s(5070) =< aux(262)
s(5070) =< aux(263)
s(5071) =< aux(262)* (6/5)
s(5072) =< aux(264)
s(5073) =< aux(262)
s(5074) =< s(5071)
s(5075) =< s(5071)
s(5073) =< s(5071)
s(5075) =< aux(263)
s(5073) =< aux(263)
s(5073) =< s(5058)* (1/3)+aux(262)
s(5074) =< s(5058)* (1/5)+s(5071)
s(5075) =< s(5058)* (1/5)+s(5071)
s(5073) =< s(5058)* (1/5)+s(5071)
s(5076) =< aux(270)
s(5077) =< aux(272)
s(5078) =< aux(272)
s(5076) =< aux(272)
s(5078) =< aux(262)
s(5076) =< aux(262)
s(5076) =< s(5058)* (1/3)+aux(270)
s(5077) =< s(5058)* (1/5)+aux(272)
s(5078) =< s(5058)* (1/5)+aux(272)
s(5076) =< s(5058)* (1/5)+aux(272)
s(5079) =< aux(265)
s(5080) =< aux(265)
s(5079) =< aux(269)
s(5080) =< aux(269)
s(5079) =< aux(272)
s(5080) =< aux(272)
s(5081) =< aux(269)* (1/2)+1/2
s(5082) =< s(5080)*aux(269)
s(5083) =< s(5079)*2
s(5084) =< s(5080)*s(5081)
s(5085) =< s(5084)* (4/5)
s(5086) =< s(5084)* (2/3)
s(5087) =< s(5084)
s(5088) =< s(5086)
s(5089) =< s(5085)
s(5090) =< s(5085)
s(5088) =< s(5085)
s(5090) =< s(5079)
s(5088) =< s(5079)
s(5091) =< s(5079)
s(5092) =< s(5083)
s(5088) =< s(5092)* (1/3)+s(5086)
s(5089) =< s(5092)* (1/5)+s(5085)
s(5090) =< s(5092)* (1/5)+s(5085)
s(5088) =< s(5092)* (1/5)+s(5085)
s(5093) =< s(5082)
s(5094) =< aux(269)
s(5094) =< aux(270)
s(5094) =< aux(273)
s(5095) =< aux(274)* (6/5)
s(5096) =< aux(273)
s(5097) =< aux(274)
s(5098) =< s(5095)
s(5099) =< s(5095)
s(5097) =< s(5095)
s(5099) =< aux(263)
s(5097) =< aux(263)
s(5097) =< s(5058)* (1/3)+aux(274)
s(5098) =< s(5058)* (1/5)+s(5095)
s(5099) =< s(5058)* (1/5)+s(5095)
s(5097) =< s(5058)* (1/5)+s(5095)
s(5100) =< aux(275)
s(5101) =< aux(276)
s(5102) =< aux(276)
s(5100) =< aux(276)
s(5102) =< aux(262)
s(5100) =< aux(262)
s(5100) =< s(5058)* (1/3)+aux(275)
s(5101) =< s(5058)* (1/5)+aux(276)
s(5102) =< s(5058)* (1/5)+aux(276)
s(5100) =< s(5058)* (1/5)+aux(276)
s(5431) =< aux(270)
s(5431) =< aux(252)
s(5433) =< aux(252)
s(5434) =< aux(252)* (1/2)
s(5435) =< aux(268)* (6/5)
s(5437) =< aux(268)
s(5438) =< s(5435)
s(5439) =< s(5435)
s(5437) =< s(5435)
s(5439) =< aux(252)
s(5437) =< aux(252)
s(5440) =< aux(252)
s(5440) =< s(5434)
s(5437) =< s(5433)* (1/3)+aux(268)
s(5438) =< s(5433)* (1/5)+s(5435)
s(5439) =< s(5433)* (1/5)+s(5435)
s(5437) =< s(5433)* (1/5)+s(5435)
s(5441) =< aux(265)
s(5442) =< aux(267)
s(5443) =< aux(255)
s(5444) =< aux(255)
s(5442) =< aux(255)
s(5444) =< aux(265)
s(5442) =< aux(265)
s(5445) =< aux(265)
s(5445) =< aux(252)
s(5442) =< s(5433)* (1/3)+aux(267)
s(5443) =< s(5433)* (1/5)+aux(255)
s(5444) =< s(5433)* (1/5)+aux(255)
s(5442) =< s(5433)* (1/5)+aux(255)
s(5446) =< aux(267)
s(5447) =< aux(267)
s(5447) =< s(5418)
s(5448) =< s(5418)
s(5449) =< s(5418)* (1/2)
s(5451) =< aux(268)
s(5452) =< s(5435)
s(5453) =< s(5435)
s(5451) =< s(5435)
s(5453) =< s(5418)
s(5451) =< s(5418)
s(5454) =< s(5418)
s(5454) =< s(5449)
s(5451) =< s(5448)* (1/3)+aux(268)
s(5452) =< s(5448)* (1/5)+s(5435)
s(5453) =< s(5448)* (1/5)+s(5435)
s(5451) =< s(5448)* (1/5)+s(5435)
s(5455) =< aux(267)
s(5456) =< aux(255)
s(5457) =< aux(255)
s(5455) =< aux(255)
s(5457) =< aux(267)
s(5455) =< s(5448)* (1/3)+aux(267)
s(5456) =< s(5448)* (1/5)+aux(255)
s(5457) =< s(5448)* (1/5)+aux(255)
s(5455) =< s(5448)* (1/5)+aux(255)
s(5458) =< aux(267)+1
s(5459) =< aux(267)
s(5461) =< aux(267)+3
s(5462) =< aux(267)* (1/2)+1/2
s(5463) =< aux(267)* (1/2)
s(5464) =< aux(267)*2
s(5465) =< s(5446)*aux(267)
s(5466) =< s(5446)*s(5458)
s(5467) =< s(5446)*s(5459)
s(5469) =< s(5446)*s(5461)
s(5470) =< s(5465)* (6/5)
s(5471) =< s(5446)*s(5462)
s(5472) =< s(5466)* (1/2)
s(5473) =< s(5467)* (6/5)
s(5474) =< s(5466)* (2/5)
s(5475) =< s(5466)* (1/3)
s(5476) =< s(5469)* (1/3)
s(5477) =< s(5466)*2
s(5478) =< s(5467)
s(5479) =< s(5464)
s(5480) =< s(5467)
s(5480) =< s(5466)
s(5481) =< s(5466)
s(5482) =< s(5466)
s(5482) =< s(5464)
s(5481) =< aux(267)
s(5483) =< s(5464)* (1/2)
s(5484) =< s(5469)* (6/5)
s(5485) =< s(5466)
s(5486) =< s(5469)
s(5487) =< s(5484)
s(5488) =< s(5484)
s(5486) =< s(5484)
s(5488) =< s(5464)
s(5486) =< s(5464)
s(5489) =< s(5464)
s(5489) =< s(5483)
s(5486) =< s(5479)* (1/3)+s(5469)
s(5487) =< s(5479)* (1/5)+s(5484)
s(5488) =< s(5479)* (1/5)+s(5484)
s(5486) =< s(5479)* (1/5)+s(5484)
s(5490) =< aux(267)
s(5490) =< s(5464)
s(5491) =< aux(267)* (6/5)
s(5492) =< s(5463)
s(5493) =< aux(267)
s(5494) =< s(5491)
s(5495) =< s(5491)
s(5493) =< s(5491)
s(5495) =< s(5464)
s(5493) =< s(5464)
s(5493) =< s(5479)* (1/3)+aux(267)
s(5494) =< s(5479)* (1/5)+s(5491)
s(5495) =< s(5479)* (1/5)+s(5491)
s(5493) =< s(5479)* (1/5)+s(5491)
s(5496) =< s(5466)
s(5497) =< s(5477)
s(5498) =< s(5477)
s(5496) =< s(5477)
s(5498) =< aux(267)
s(5496) =< aux(267)
s(5496) =< s(5479)* (1/3)+s(5466)
s(5497) =< s(5479)* (1/5)+s(5477)
s(5498) =< s(5479)* (1/5)+s(5477)
s(5496) =< s(5479)* (1/5)+s(5477)
s(5499) =< s(5467)
s(5500) =< s(5467)
s(5499) =< s(5477)
s(5500) =< s(5477)
s(5501) =< s(5500)*aux(267)
s(5502) =< s(5499)*2
s(5503) =< s(5500)*s(5462)
s(5504) =< s(5503)* (4/5)
s(5505) =< s(5503)* (2/3)
s(5506) =< s(5503)
s(5507) =< s(5505)
s(5508) =< s(5504)
s(5509) =< s(5504)
s(5507) =< s(5504)
s(5509) =< s(5499)
s(5507) =< s(5499)
s(5510) =< s(5499)
s(5511) =< s(5502)
s(5507) =< s(5511)* (1/3)+s(5505)
s(5508) =< s(5511)* (1/5)+s(5504)
s(5509) =< s(5511)* (1/5)+s(5504)
s(5507) =< s(5511)* (1/5)+s(5504)
s(5512) =< s(5501)
s(5513) =< s(5467)
s(5513) =< s(5466)
s(5513) =< s(5472)
s(5514) =< s(5476)* (6/5)
s(5515) =< s(5472)
s(5516) =< s(5476)
s(5517) =< s(5514)
s(5518) =< s(5514)
s(5516) =< s(5514)
s(5518) =< s(5464)
s(5516) =< s(5464)
s(5516) =< s(5479)* (1/3)+s(5476)
s(5517) =< s(5479)* (1/5)+s(5514)
s(5518) =< s(5479)* (1/5)+s(5514)
s(5516) =< s(5479)* (1/5)+s(5514)
s(5519) =< s(5475)
s(5520) =< s(5474)
s(5521) =< s(5474)
s(5519) =< s(5474)
s(5521) =< aux(267)
s(5519) =< aux(267)
s(5519) =< s(5479)* (1/3)+s(5475)
s(5520) =< s(5479)* (1/5)+s(5474)
s(5521) =< s(5479)* (1/5)+s(5474)
s(5519) =< s(5479)* (1/5)+s(5474)
s(5522) =< s(5467)
s(5523) =< s(5473)
s(5524) =< s(5473)
s(5522) =< s(5473)
s(5524) =< s(5467)
s(5525) =< s(5467)
s(5525) =< s(5472)
s(5522) =< s(5485)* (1/3)+s(5467)
s(5523) =< s(5485)* (1/5)+s(5473)
s(5524) =< s(5485)* (1/5)+s(5473)
s(5522) =< s(5485)* (1/5)+s(5473)
s(5526) =< s(5467)
s(5527) =< s(5467)
s(5526) =< aux(267)
s(5527) =< aux(267)
s(5528) =< s(5527)*aux(267)
s(5529) =< s(5526)*2
s(5530) =< s(5527)*s(5462)
s(5531) =< s(5530)* (4/5)
s(5532) =< s(5530)* (2/3)
s(5533) =< s(5530)
s(5534) =< s(5532)
s(5535) =< s(5531)
s(5536) =< s(5531)
s(5534) =< s(5531)
s(5536) =< s(5526)
s(5534) =< s(5526)
s(5537) =< s(5526)
s(5538) =< s(5529)
s(5534) =< s(5538)* (1/3)+s(5532)
s(5535) =< s(5538)* (1/5)+s(5531)
s(5536) =< s(5538)* (1/5)+s(5531)
s(5534) =< s(5538)* (1/5)+s(5531)
s(5539) =< s(5528)
s(5540) =< s(5459)* (1/2)+1/2
s(5541) =< s(5500)*s(5459)
s(5542) =< s(5500)*s(5540)
s(5543) =< s(5542)* (4/5)
s(5544) =< s(5542)* (2/3)
s(5545) =< s(5542)
s(5546) =< s(5544)
s(5547) =< s(5543)
s(5548) =< s(5543)
s(5546) =< s(5543)
s(5548) =< s(5499)
s(5546) =< s(5499)
s(5546) =< s(5511)* (1/3)+s(5544)
s(5547) =< s(5511)* (1/5)+s(5543)
s(5548) =< s(5511)* (1/5)+s(5543)
s(5546) =< s(5511)* (1/5)+s(5543)
s(5549) =< s(5541)
s(5550) =< s(5471)
s(5551) =< s(5465)
s(5552) =< s(5470)
s(5553) =< s(5470)
s(5551) =< s(5470)
s(5553) =< s(5467)
s(5551) =< s(5467)
s(5551) =< s(5485)* (1/3)+s(5465)
s(5552) =< s(5485)* (1/5)+s(5470)
s(5553) =< s(5485)* (1/5)+s(5470)
s(5551) =< s(5485)* (1/5)+s(5470)
s(5554) =< aux(268)
s(5555) =< aux(267)
s(5556) =< aux(267)
s(5555) =< aux(268)
s(5556) =< aux(268)
s(5557) =< s(5555)* (1/2)
s(5558) =< s(5555)*2
s(5559) =< s(5556)*aux(267)
s(5560) =< s(5556)*s(5458)
s(5561) =< s(5556)*s(5459)
s(5563) =< s(5556)*s(5461)
s(5564) =< s(5559)* (6/5)
s(5565) =< s(5556)*s(5462)
s(5566) =< s(5560)* (1/2)
s(5567) =< s(5561)* (6/5)
s(5568) =< s(5560)* (2/5)
s(5569) =< s(5560)* (1/3)
s(5570) =< s(5563)* (1/3)
s(5571) =< s(5560)*2
s(5572) =< s(5561)
s(5573) =< s(5555)
s(5574) =< s(5558)
s(5575) =< s(5561)
s(5575) =< s(5560)
s(5576) =< s(5560)
s(5577) =< s(5560)
s(5577) =< s(5558)
s(5576) =< s(5555)
s(5578) =< s(5558)* (1/2)
s(5579) =< s(5563)* (6/5)
s(5580) =< s(5560)
s(5581) =< s(5563)
s(5582) =< s(5579)
s(5583) =< s(5579)
s(5581) =< s(5579)
s(5583) =< s(5558)
s(5581) =< s(5558)
s(5584) =< s(5558)
s(5584) =< s(5578)
s(5581) =< s(5574)* (1/3)+s(5563)
s(5582) =< s(5574)* (1/5)+s(5579)
s(5583) =< s(5574)* (1/5)+s(5579)
s(5581) =< s(5574)* (1/5)+s(5579)
s(5585) =< s(5555)
s(5585) =< s(5558)
s(5586) =< s(5555)* (6/5)
s(5587) =< s(5557)
s(5588) =< s(5555)
s(5589) =< s(5586)
s(5590) =< s(5586)
s(5588) =< s(5586)
s(5590) =< s(5558)
s(5588) =< s(5558)
s(5588) =< s(5574)* (1/3)+s(5555)
s(5589) =< s(5574)* (1/5)+s(5586)
s(5590) =< s(5574)* (1/5)+s(5586)
s(5588) =< s(5574)* (1/5)+s(5586)
s(5591) =< s(5560)
s(5592) =< s(5571)
s(5593) =< s(5571)
s(5591) =< s(5571)
s(5593) =< s(5555)
s(5591) =< s(5555)
s(5591) =< s(5574)* (1/3)+s(5560)
s(5592) =< s(5574)* (1/5)+s(5571)
s(5593) =< s(5574)* (1/5)+s(5571)
s(5591) =< s(5574)* (1/5)+s(5571)
s(5594) =< s(5561)
s(5595) =< s(5561)
s(5594) =< s(5571)
s(5595) =< s(5571)
s(5596) =< s(5595)*aux(267)
s(5597) =< s(5594)*2
s(5598) =< s(5595)*s(5462)
s(5599) =< s(5598)* (4/5)
s(5600) =< s(5598)* (2/3)
s(5601) =< s(5598)
s(5602) =< s(5600)
s(5603) =< s(5599)
s(5604) =< s(5599)
s(5602) =< s(5599)
s(5604) =< s(5594)
s(5602) =< s(5594)
s(5605) =< s(5594)
s(5606) =< s(5597)
s(5602) =< s(5606)* (1/3)+s(5600)
s(5603) =< s(5606)* (1/5)+s(5599)
s(5604) =< s(5606)* (1/5)+s(5599)
s(5602) =< s(5606)* (1/5)+s(5599)
s(5607) =< s(5596)
s(5608) =< s(5561)
s(5608) =< s(5560)
s(5608) =< s(5566)
s(5609) =< s(5570)* (6/5)
s(5610) =< s(5566)
s(5611) =< s(5570)
s(5612) =< s(5609)
s(5613) =< s(5609)
s(5611) =< s(5609)
s(5613) =< s(5558)
s(5611) =< s(5558)
s(5611) =< s(5574)* (1/3)+s(5570)
s(5612) =< s(5574)* (1/5)+s(5609)
s(5613) =< s(5574)* (1/5)+s(5609)
s(5611) =< s(5574)* (1/5)+s(5609)
s(5614) =< s(5569)
s(5615) =< s(5568)
s(5616) =< s(5568)
s(5614) =< s(5568)
s(5616) =< s(5555)
s(5614) =< s(5555)
s(5614) =< s(5574)* (1/3)+s(5569)
s(5615) =< s(5574)* (1/5)+s(5568)
s(5616) =< s(5574)* (1/5)+s(5568)
s(5614) =< s(5574)* (1/5)+s(5568)
s(5617) =< s(5561)
s(5618) =< s(5567)
s(5619) =< s(5567)
s(5617) =< s(5567)
s(5619) =< s(5561)
s(5620) =< s(5561)
s(5620) =< s(5566)
s(5617) =< s(5580)* (1/3)+s(5561)
s(5618) =< s(5580)* (1/5)+s(5567)
s(5619) =< s(5580)* (1/5)+s(5567)
s(5617) =< s(5580)* (1/5)+s(5567)
s(5621) =< s(5561)
s(5622) =< s(5561)
s(5621) =< s(5555)
s(5622) =< s(5555)
s(5623) =< s(5622)*aux(267)
s(5624) =< s(5621)*2
s(5625) =< s(5622)*s(5462)
s(5626) =< s(5625)* (4/5)
s(5627) =< s(5625)* (2/3)
s(5628) =< s(5625)
s(5629) =< s(5627)
s(5630) =< s(5626)
s(5631) =< s(5626)
s(5629) =< s(5626)
s(5631) =< s(5621)
s(5629) =< s(5621)
s(5632) =< s(5621)
s(5633) =< s(5624)
s(5629) =< s(5633)* (1/3)+s(5627)
s(5630) =< s(5633)* (1/5)+s(5626)
s(5631) =< s(5633)* (1/5)+s(5626)
s(5629) =< s(5633)* (1/5)+s(5626)
s(5634) =< s(5623)
s(5635) =< s(5595)*s(5459)
s(5636) =< s(5595)*s(5540)
s(5637) =< s(5636)* (4/5)
s(5638) =< s(5636)* (2/3)
s(5639) =< s(5636)
s(5640) =< s(5638)
s(5641) =< s(5637)
s(5642) =< s(5637)
s(5640) =< s(5637)
s(5642) =< s(5594)
s(5640) =< s(5594)
s(5640) =< s(5606)* (1/3)+s(5638)
s(5641) =< s(5606)* (1/5)+s(5637)
s(5642) =< s(5606)* (1/5)+s(5637)
s(5640) =< s(5606)* (1/5)+s(5637)
s(5643) =< s(5635)
s(5644) =< s(5565)
s(5645) =< s(5559)
s(5646) =< s(5564)
s(5647) =< s(5564)
s(5645) =< s(5564)
s(5647) =< s(5561)
s(5645) =< s(5561)
s(5645) =< s(5580)* (1/3)+s(5559)
s(5646) =< s(5580)* (1/5)+s(5564)
s(5647) =< s(5580)* (1/5)+s(5564)
s(5645) =< s(5580)* (1/5)+s(5564)
s(5401) =< aux(265)
s(5402) =< aux(265)
s(5401) =< aux(267)
s(5402) =< aux(267)
s(5401) =< aux(269)
s(5402) =< aux(269)
s(5404) =< s(5402)*aux(269)
s(5405) =< s(5401)*2
s(5406) =< s(5402)*s(5081)
s(5407) =< s(5406)* (4/5)
s(5408) =< s(5406)* (2/3)
s(5409) =< s(5406)
s(5410) =< s(5408)
s(5411) =< s(5407)
s(5412) =< s(5407)
s(5410) =< s(5407)
s(5412) =< s(5401)
s(5410) =< s(5401)
s(5413) =< s(5401)
s(5414) =< s(5405)
s(5410) =< s(5414)* (1/3)+s(5408)
s(5411) =< s(5414)* (1/5)+s(5407)
s(5412) =< s(5414)* (1/5)+s(5407)
s(5410) =< s(5414)* (1/5)+s(5407)
s(5415) =< s(5404)
s(5656) =< aux(265)
s(5657) =< aux(265)
s(5656) =< aux(269)
s(5657) =< aux(269)
s(5659) =< s(5657)*aux(269)
s(5660) =< s(5656)*2
s(5661) =< s(5657)*s(5081)
s(5662) =< s(5661)* (4/5)
s(5663) =< s(5661)* (2/3)
s(5664) =< s(5661)
s(5665) =< s(5663)
s(5666) =< s(5662)
s(5667) =< s(5662)
s(5665) =< s(5662)
s(5667) =< s(5656)
s(5665) =< s(5656)
s(5668) =< s(5656)
s(5669) =< s(5660)
s(5665) =< s(5669)* (1/3)+s(5663)
s(5666) =< s(5669)* (1/5)+s(5662)
s(5667) =< s(5669)* (1/5)+s(5662)
s(5665) =< s(5669)* (1/5)+s(5662)
s(5670) =< s(5659)
s(5679) =< aux(265)
s(5680) =< aux(265)
s(5679) =< aux(266)
s(5680) =< aux(266)
s(5679) =< aux(269)
s(5680) =< aux(269)
s(5682) =< s(5680)*aux(269)
s(5683) =< s(5679)*2
s(5684) =< s(5680)*s(5081)
s(5685) =< s(5684)* (4/5)
s(5686) =< s(5684)* (2/3)
s(5687) =< s(5684)
s(5688) =< s(5686)
s(5689) =< s(5685)
s(5690) =< s(5685)
s(5688) =< s(5685)
s(5690) =< s(5679)
s(5688) =< s(5679)
s(5691) =< s(5679)
s(5692) =< s(5683)
s(5688) =< s(5692)* (1/3)+s(5686)
s(5689) =< s(5692)* (1/5)+s(5685)
s(5690) =< s(5692)* (1/5)+s(5685)
s(5688) =< s(5692)* (1/5)+s(5685)
s(5693) =< s(5682)
s(5729) =< aux(265)
s(5730) =< aux(265)
s(5729) =< aux(268)
s(5730) =< aux(268)
s(5729) =< aux(269)
s(5730) =< aux(269)
s(5732) =< s(5730)*aux(269)
s(5733) =< s(5729)*2
s(5734) =< s(5730)*s(5081)
s(5735) =< s(5734)* (4/5)
s(5736) =< s(5734)* (2/3)
s(5737) =< s(5734)
s(5738) =< s(5736)
s(5739) =< s(5735)
s(5740) =< s(5735)
s(5738) =< s(5735)
s(5740) =< s(5729)
s(5738) =< s(5729)
s(5741) =< s(5729)
s(5742) =< s(5733)
s(5738) =< s(5742)* (1/3)+s(5736)
s(5739) =< s(5742)* (1/5)+s(5735)
s(5740) =< s(5742)* (1/5)+s(5735)
s(5738) =< s(5742)* (1/5)+s(5735)
s(5743) =< s(5732)
s(5118) =< aux(270)
s(5118) =< aux(264)
s(5121) =< aux(262)* (1/2)
s(5122) =< s(5108)* (6/5)
s(5124) =< s(5108)
s(5125) =< s(5122)
s(5126) =< s(5122)
s(5124) =< s(5122)
s(5126) =< aux(262)
s(5124) =< aux(262)
s(5127) =< aux(262)
s(5127) =< s(5121)
s(5124) =< s(5057)* (1/3)+s(5108)
s(5125) =< s(5057)* (1/5)+s(5122)
s(5126) =< s(5057)* (1/5)+s(5122)
s(5124) =< s(5057)* (1/5)+s(5122)
s(5130) =< s(5109)
s(5130) =< s(5057)* (1/5)+s(5109)
s(5136) =< aux(270)* (1/2)
s(5137) =< s(5114)* (6/5)
s(5138) =< s(5114)
s(5139) =< s(5137)
s(5140) =< s(5137)
s(5138) =< s(5137)
s(5140) =< aux(270)
s(5138) =< aux(270)
s(5141) =< aux(270)
s(5141) =< s(5136)
s(5138) =< s(5065)* (1/3)+s(5114)
s(5139) =< s(5065)* (1/5)+s(5137)
s(5140) =< s(5065)* (1/5)+s(5137)
s(5138) =< s(5065)* (1/5)+s(5137)
s(5142) =< aux(269)
s(5143) =< s(5106)
s(5144) =< s(5106)
s(5142) =< s(5106)
s(5144) =< aux(269)
s(5142) =< s(5065)* (1/3)+aux(269)
s(5143) =< s(5065)* (1/5)+s(5106)
s(5144) =< s(5065)* (1/5)+s(5106)
s(5142) =< s(5065)* (1/5)+s(5106)
s(5145) =< aux(269)+1
s(5146) =< aux(269)
s(5147) =< s(5115)
s(5148) =< aux(269)+3
s(5150) =< aux(269)* (1/2)
s(5151) =< aux(269)*2
s(5152) =< s(5059)*s(5115)
s(5153) =< s(5059)*s(5145)
s(5154) =< s(5059)*s(5146)
s(5155) =< s(5059)*s(5147)
s(5156) =< s(5059)*s(5148)
s(5157) =< s(5152)* (6/5)
s(5158) =< s(5059)*s(5081)
s(5159) =< s(5153)* (1/2)
s(5160) =< s(5155)* (6/5)
s(5161) =< s(5153)* (2/5)
s(5162) =< s(5153)* (1/3)
s(5163) =< s(5156)* (1/3)
s(5164) =< s(5153)*2
s(5165) =< s(5154)
s(5166) =< s(5151)
s(5167) =< s(5154)
s(5167) =< s(5153)
s(5168) =< s(5153)
s(5169) =< s(5153)
s(5169) =< s(5151)
s(5168) =< aux(269)
s(5170) =< s(5151)* (1/2)
s(5171) =< s(5156)* (6/5)
s(5172) =< s(5153)
s(5173) =< s(5156)
s(5174) =< s(5171)
s(5175) =< s(5171)
s(5173) =< s(5171)
s(5175) =< s(5151)
s(5173) =< s(5151)
s(5176) =< s(5151)
s(5176) =< s(5170)
s(5173) =< s(5166)* (1/3)+s(5156)
s(5174) =< s(5166)* (1/5)+s(5171)
s(5175) =< s(5166)* (1/5)+s(5171)
s(5173) =< s(5166)* (1/5)+s(5171)
s(5177) =< aux(269)
s(5177) =< s(5151)
s(5178) =< aux(269)* (6/5)
s(5179) =< s(5150)
s(5180) =< aux(269)
s(5181) =< s(5178)
s(5182) =< s(5178)
s(5180) =< s(5178)
s(5182) =< s(5151)
s(5180) =< s(5151)
s(5180) =< s(5166)* (1/3)+aux(269)
s(5181) =< s(5166)* (1/5)+s(5178)
s(5182) =< s(5166)* (1/5)+s(5178)
s(5180) =< s(5166)* (1/5)+s(5178)
s(5183) =< s(5153)
s(5184) =< s(5164)
s(5185) =< s(5164)
s(5183) =< s(5164)
s(5185) =< aux(269)
s(5183) =< aux(269)
s(5183) =< s(5166)* (1/3)+s(5153)
s(5184) =< s(5166)* (1/5)+s(5164)
s(5185) =< s(5166)* (1/5)+s(5164)
s(5183) =< s(5166)* (1/5)+s(5164)
s(5186) =< s(5154)
s(5187) =< s(5154)
s(5186) =< s(5164)
s(5187) =< s(5164)
s(5188) =< s(5187)*aux(269)
s(5189) =< s(5186)*2
s(5190) =< s(5187)*s(5081)
s(5191) =< s(5190)* (4/5)
s(5192) =< s(5190)* (2/3)
s(5193) =< s(5190)
s(5194) =< s(5192)
s(5195) =< s(5191)
s(5196) =< s(5191)
s(5194) =< s(5191)
s(5196) =< s(5186)
s(5194) =< s(5186)
s(5197) =< s(5186)
s(5198) =< s(5189)
s(5194) =< s(5198)* (1/3)+s(5192)
s(5195) =< s(5198)* (1/5)+s(5191)
s(5196) =< s(5198)* (1/5)+s(5191)
s(5194) =< s(5198)* (1/5)+s(5191)
s(5199) =< s(5188)
s(5200) =< s(5154)
s(5200) =< s(5153)
s(5200) =< s(5159)
s(5201) =< s(5163)* (6/5)
s(5202) =< s(5159)
s(5203) =< s(5163)
s(5204) =< s(5201)
s(5205) =< s(5201)
s(5203) =< s(5201)
s(5205) =< s(5151)
s(5203) =< s(5151)
s(5203) =< s(5166)* (1/3)+s(5163)
s(5204) =< s(5166)* (1/5)+s(5201)
s(5205) =< s(5166)* (1/5)+s(5201)
s(5203) =< s(5166)* (1/5)+s(5201)
s(5206) =< s(5162)
s(5207) =< s(5161)
s(5208) =< s(5161)
s(5206) =< s(5161)
s(5208) =< aux(269)
s(5206) =< aux(269)
s(5206) =< s(5166)* (1/3)+s(5162)
s(5207) =< s(5166)* (1/5)+s(5161)
s(5208) =< s(5166)* (1/5)+s(5161)
s(5206) =< s(5166)* (1/5)+s(5161)
s(5209) =< s(5155)
s(5210) =< s(5160)
s(5211) =< s(5160)
s(5209) =< s(5160)
s(5211) =< s(5154)
s(5209) =< s(5154)
s(5212) =< s(5154)
s(5212) =< s(5159)
s(5209) =< s(5172)* (1/3)+s(5155)
s(5210) =< s(5172)* (1/5)+s(5160)
s(5211) =< s(5172)* (1/5)+s(5160)
s(5209) =< s(5172)* (1/5)+s(5160)
s(5213) =< s(5154)
s(5214) =< s(5154)
s(5213) =< aux(269)
s(5214) =< aux(269)
s(5215) =< s(5214)*aux(269)
s(5216) =< s(5213)*2
s(5217) =< s(5214)*s(5081)
s(5218) =< s(5217)* (4/5)
s(5219) =< s(5217)* (2/3)
s(5220) =< s(5217)
s(5221) =< s(5219)
s(5222) =< s(5218)
s(5223) =< s(5218)
s(5221) =< s(5218)
s(5223) =< s(5213)
s(5221) =< s(5213)
s(5224) =< s(5213)
s(5225) =< s(5216)
s(5221) =< s(5225)* (1/3)+s(5219)
s(5222) =< s(5225)* (1/5)+s(5218)
s(5223) =< s(5225)* (1/5)+s(5218)
s(5221) =< s(5225)* (1/5)+s(5218)
s(5226) =< s(5215)
s(5227) =< s(5146)* (1/2)+1/2
s(5228) =< s(5187)*s(5146)
s(5229) =< s(5187)*s(5227)
s(5230) =< s(5229)* (4/5)
s(5231) =< s(5229)* (2/3)
s(5232) =< s(5229)
s(5233) =< s(5231)
s(5234) =< s(5230)
s(5235) =< s(5230)
s(5233) =< s(5230)
s(5235) =< s(5186)
s(5233) =< s(5186)
s(5233) =< s(5198)* (1/3)+s(5231)
s(5234) =< s(5198)* (1/5)+s(5230)
s(5235) =< s(5198)* (1/5)+s(5230)
s(5233) =< s(5198)* (1/5)+s(5230)
s(5236) =< s(5228)
s(5237) =< s(5158)
s(5238) =< s(5152)
s(5239) =< s(5157)
s(5240) =< s(5157)
s(5238) =< s(5157)
s(5240) =< s(5154)
s(5238) =< s(5154)
s(5238) =< s(5172)* (1/3)+s(5152)
s(5239) =< s(5172)* (1/5)+s(5157)
s(5240) =< s(5172)* (1/5)+s(5157)
s(5238) =< s(5172)* (1/5)+s(5157)
s(5241) =< s(5114)
s(5242) =< aux(269)
s(5243) =< aux(269)
s(5242) =< s(5114)
s(5243) =< s(5114)
s(5244) =< s(5242)* (1/2)
s(5245) =< s(5242)*2
s(5246) =< s(5243)*s(5115)
s(5247) =< s(5243)*s(5145)
s(5248) =< s(5243)*s(5146)
s(5249) =< s(5243)*s(5147)
s(5250) =< s(5243)*s(5148)
s(5251) =< s(5246)* (6/5)
s(5252) =< s(5243)*s(5081)
s(5253) =< s(5247)* (1/2)
s(5254) =< s(5249)* (6/5)
s(5255) =< s(5247)* (2/5)
s(5256) =< s(5247)* (1/3)
s(5257) =< s(5250)* (1/3)
s(5258) =< s(5247)*2
s(5259) =< s(5248)
s(5260) =< s(5242)
s(5261) =< s(5245)
s(5262) =< s(5248)
s(5262) =< s(5247)
s(5263) =< s(5247)
s(5264) =< s(5247)
s(5264) =< s(5245)
s(5263) =< s(5242)
s(5265) =< s(5245)* (1/2)
s(5266) =< s(5250)* (6/5)
s(5267) =< s(5247)
s(5268) =< s(5250)
s(5269) =< s(5266)
s(5270) =< s(5266)
s(5268) =< s(5266)
s(5270) =< s(5245)
s(5268) =< s(5245)
s(5271) =< s(5245)
s(5271) =< s(5265)
s(5268) =< s(5261)* (1/3)+s(5250)
s(5269) =< s(5261)* (1/5)+s(5266)
s(5270) =< s(5261)* (1/5)+s(5266)
s(5268) =< s(5261)* (1/5)+s(5266)
s(5272) =< s(5242)
s(5272) =< s(5245)
s(5273) =< s(5242)* (6/5)
s(5274) =< s(5244)
s(5275) =< s(5242)
s(5276) =< s(5273)
s(5277) =< s(5273)
s(5275) =< s(5273)
s(5277) =< s(5245)
s(5275) =< s(5245)
s(5275) =< s(5261)* (1/3)+s(5242)
s(5276) =< s(5261)* (1/5)+s(5273)
s(5277) =< s(5261)* (1/5)+s(5273)
s(5275) =< s(5261)* (1/5)+s(5273)
s(5278) =< s(5247)
s(5279) =< s(5258)
s(5280) =< s(5258)
s(5278) =< s(5258)
s(5280) =< s(5242)
s(5278) =< s(5242)
s(5278) =< s(5261)* (1/3)+s(5247)
s(5279) =< s(5261)* (1/5)+s(5258)
s(5280) =< s(5261)* (1/5)+s(5258)
s(5278) =< s(5261)* (1/5)+s(5258)
s(5281) =< s(5248)
s(5282) =< s(5248)
s(5281) =< s(5258)
s(5282) =< s(5258)
s(5283) =< s(5282)*aux(269)
s(5284) =< s(5281)*2
s(5285) =< s(5282)*s(5081)
s(5286) =< s(5285)* (4/5)
s(5287) =< s(5285)* (2/3)
s(5288) =< s(5285)
s(5289) =< s(5287)
s(5290) =< s(5286)
s(5291) =< s(5286)
s(5289) =< s(5286)
s(5291) =< s(5281)
s(5289) =< s(5281)
s(5292) =< s(5281)
s(5293) =< s(5284)
s(5289) =< s(5293)* (1/3)+s(5287)
s(5290) =< s(5293)* (1/5)+s(5286)
s(5291) =< s(5293)* (1/5)+s(5286)
s(5289) =< s(5293)* (1/5)+s(5286)
s(5294) =< s(5283)
s(5295) =< s(5248)
s(5295) =< s(5247)
s(5295) =< s(5253)
s(5296) =< s(5257)* (6/5)
s(5297) =< s(5253)
s(5298) =< s(5257)
s(5299) =< s(5296)
s(5300) =< s(5296)
s(5298) =< s(5296)
s(5300) =< s(5245)
s(5298) =< s(5245)
s(5298) =< s(5261)* (1/3)+s(5257)
s(5299) =< s(5261)* (1/5)+s(5296)
s(5300) =< s(5261)* (1/5)+s(5296)
s(5298) =< s(5261)* (1/5)+s(5296)
s(5301) =< s(5256)
s(5302) =< s(5255)
s(5303) =< s(5255)
s(5301) =< s(5255)
s(5303) =< s(5242)
s(5301) =< s(5242)
s(5301) =< s(5261)* (1/3)+s(5256)
s(5302) =< s(5261)* (1/5)+s(5255)
s(5303) =< s(5261)* (1/5)+s(5255)
s(5301) =< s(5261)* (1/5)+s(5255)
s(5304) =< s(5249)
s(5305) =< s(5254)
s(5306) =< s(5254)
s(5304) =< s(5254)
s(5306) =< s(5248)
s(5304) =< s(5248)
s(5307) =< s(5248)
s(5307) =< s(5253)
s(5304) =< s(5267)* (1/3)+s(5249)
s(5305) =< s(5267)* (1/5)+s(5254)
s(5306) =< s(5267)* (1/5)+s(5254)
s(5304) =< s(5267)* (1/5)+s(5254)
s(5308) =< s(5248)
s(5309) =< s(5248)
s(5308) =< s(5242)
s(5309) =< s(5242)
s(5310) =< s(5309)*aux(269)
s(5311) =< s(5308)*2
s(5312) =< s(5309)*s(5081)
s(5313) =< s(5312)* (4/5)
s(5314) =< s(5312)* (2/3)
s(5315) =< s(5312)
s(5316) =< s(5314)
s(5317) =< s(5313)
s(5318) =< s(5313)
s(5316) =< s(5313)
s(5318) =< s(5308)
s(5316) =< s(5308)
s(5319) =< s(5308)
s(5320) =< s(5311)
s(5316) =< s(5320)* (1/3)+s(5314)
s(5317) =< s(5320)* (1/5)+s(5313)
s(5318) =< s(5320)* (1/5)+s(5313)
s(5316) =< s(5320)* (1/5)+s(5313)
s(5321) =< s(5310)
s(5322) =< s(5282)*s(5146)
s(5323) =< s(5282)*s(5227)
s(5324) =< s(5323)* (4/5)
s(5325) =< s(5323)* (2/3)
s(5326) =< s(5323)
s(5327) =< s(5325)
s(5328) =< s(5324)
s(5329) =< s(5324)
s(5327) =< s(5324)
s(5329) =< s(5281)
s(5327) =< s(5281)
s(5327) =< s(5293)* (1/3)+s(5325)
s(5328) =< s(5293)* (1/5)+s(5324)
s(5329) =< s(5293)* (1/5)+s(5324)
s(5327) =< s(5293)* (1/5)+s(5324)
s(5330) =< s(5322)
s(5331) =< s(5252)
s(5332) =< s(5246)
s(5333) =< s(5251)
s(5334) =< s(5251)
s(5332) =< s(5251)
s(5334) =< s(5248)
s(5332) =< s(5248)
s(5332) =< s(5267)* (1/3)+s(5246)
s(5333) =< s(5267)* (1/5)+s(5251)
s(5334) =< s(5267)* (1/5)+s(5251)
s(5332) =< s(5267)* (1/5)+s(5251)
with precondition: [V=2,V1>=0,V35>=0]
* Chain [66]: 2
with precondition: [V1=0,V>=1]
Closed-form bounds of start(V,V1,V35):
-------------------------------------
* Chain [74] with precondition: [V>=0]
- Upper bound: 199/5*V+534/5+nat(V1)*82+129/5*nat(V1)*V+nat(V+V1)*2808+nat(V+V1)*2156*nat(V+V1)+nat(V+V1)*258*nat(V+V1)*nat(V+V1)+ (6*V+6)+nat(V1+1)*47+6/5*nat(V1+3)+nat(2*V+2*V1)*16+nat(2*V1+2)+nat(2/5*V+2/5*V1)*18+nat(2/5*V1+2/5)+nat(V+V1+1)*50+54/5*nat(V+V1+2)+51/5*nat(V/3+V1/3+2/3)+ (6*V+6)+nat(V/3+V1/3)*9+nat(V/3+V1/3)*136*nat(V+V1)+nat(V1/2+1/2)*2+6/5*nat(V1/3+1)
- Complexity: n^3
* Chain [73] with precondition: [V=1,V1>=0,V35>=0]
- Upper bound: 13221/5*V1+3873/5+3527/2*V1*V1+1032/5*V1*V1*V1+903/10*V1*V35+2941/2*V35+1161/10*V35*V1+4312/5*V35*V35+516/5*V35*V35*V35+32*V1+18*V35+32/5*V1+2*V35+ (4224*V1+4224*V35)+ (3438*V1+3438*V35)* (V1+V35)+ (V1+V35)* ((387*V1+387*V35)* (V1+V35))+ (148*V1+148)+ (44/5*V1+88/5)+ (12/5*V1+36/5)+ (47*V35+47)+ (28/5*V35+56/5)+ (12/5*V35+36/5)+ (4*V1+4)+ (96*V1+96*V35)+ (4*V35+4)+ (4/5*V1+4/5)+ (4/5*V35+4/5)+ (75*V1+75*V35+75)+ (132/5*V1+132/5*V35+264/5)+ (2*V1+2)+ (4/5*V1+12/5)+ (34/15*V1+68/15)+ (7*V35+7)+ (4/5*V35+12/5)+ (4/5*V35+8/5)+8/3*V1+544/15*V1*V1+V35+272/15*V35*V35
- Complexity: n^3
* Chain [72] with precondition: [V=V1,V>=1]
- Upper bound: 10*V1+7
- Complexity: n
* Chain [71] with precondition: [V=1,V1=2]
- Upper bound: 0
- Complexity: constant
* Chain [70] with precondition: [V=1,V35=0,V1>=1]
- Upper bound: 1711/10
- Complexity: constant
* Chain [69] with precondition: [V=2,V1=1]
- Upper bound: 0
- Complexity: constant
* Chain [68] with precondition: [V=2,V1=2]
- Upper bound: 0
- Complexity: constant
* Chain [67] with precondition: [V=2,V1>=0,V35>=0]
- Upper bound: 973/10*V1+6476/5*V35+2521/10+903/10*V35*V1+4312/5*V35*V35+516/5*V35*V35*V35+16*V35+8/5*V35+ (1408*V1+1408*V35)+ (1146*V1+1146*V35)* (V1+V35)+ (V1+V35)* ((129*V1+129*V35)* (V1+V35))+ (18*V1+18)+ (33*V35+33)+ (22/5*V35+44/5)+ (12/5*V35+36/5)+ (32*V1+32*V35)+ (4*V35+4)+ (4/5*V35+4/5)+ (25*V1+25*V35+25)+ (44/5*V1+44/5*V35+88/5)+ (7*V35+7)+ (4/5*V35+12/5)+ (2/5*V35+4/5)+272/15*V35*V35
- Complexity: n^3
* Chain [66] with precondition: [V1=0,V>=1]
- Upper bound: 2
- Complexity: constant
### Maximum cost of start(V,V1,V35): max([1711/10,524/5+nat(V1)*77+nat(V1+1)*13+max([199/5*V+129/5*nat(V1)*V+nat(V+V1)*2808+nat(V+V1)*2156*nat(V+V1)+nat(V+V1)*258*nat(V+V1)*nat(V+V1)+ (6*V+6)+nat(V1+1)*29+6/5*nat(V1+3)+nat(2*V+2*V1)*16+nat(2*V1+2)+nat(2/5*V+2/5*V1)*18+nat(2/5*V1+2/5)+nat(V+V1+1)*50+54/5*nat(V+V1+2)+51/5*nat(V/3+V1/3+2/3)+ (6*V+6)+nat(V/3+V1/3)*9+nat(V/3+V1/3)*136*nat(V+V1)+nat(V1/2+1/2)*2+6/5*nat(V1/3+1),1453/10+153/10*nat(V1)+6476/5*nat(V35)+903/10*nat(V35)*nat(V1)+4312/5*nat(V35)*nat(V35)+516/5*nat(V35)*nat(V35)*nat(V35)+nat(2*V35)*8+nat(2/5*V35)*4+nat(V1+V35)*1408+nat(V1+V35)*1146*nat(V1+V35)+nat(V1+V35)*129*nat(V1+V35)*nat(V1+V35)+nat(V35+1)*33+22/5*nat(V35+2)+12/5*nat(V35+3)+nat(2*V1+2*V35)*16+nat(2*V35+2)*2+nat(2/5*V35+2/5)*2+nat(V1+V35+1)*25+44/5*nat(V1+V35+2)+nat(V35/2+1/2)*14+12/5*nat(V35/3+1)+6/5*nat(V35/3+2/3)+272/5*nat(V35/3)*nat(V35)+ (1045/2+25469/10*nat(V1)+3527/2*nat(V1)*nat(V1)+1032/5*nat(V1)*nat(V1)*nat(V1)+903/10*nat(V1)*nat(V35)+1753/10*nat(V35)+129/5*nat(V35)*nat(V1)+nat(2*V1)*16+nat(2*V35)+nat(2/5*V1)*16+nat(2/5*V35)+nat(V1+V35)*2816+nat(V1+V35)*2292*nat(V1+V35)+nat(V1+V35)*258*nat(V1+V35)*nat(V1+V35)+nat(V1+1)*130+44/5*nat(V1+2)+12/5*nat(V1+3)+nat(V35+1)*14+6/5*nat(V35+2)+nat(2*V1+2)*2+nat(2*V1+2*V35)*32+nat(2/5*V1+2/5)*2+nat(V1+V35+1)*50+88/5*nat(V1+V35+2)+nat(V1/2+1/2)*4+12/5*nat(V1/3+1)+34/5*nat(V1/3+2/3)+6/5*nat(V35/3+2/3)+nat(V1/3)*8+544/5*nat(V1/3)*nat(V1)+nat(V35/2)*2)])+ (nat(V1)*5+2+nat(V1+1)*5)])
Asymptotic class: n^3
* Total analysis performed in 95742 ms.